Library MetaRocq.Utils.MRTactics.FindHyp

Ltac find_hyp_eq a b := match goal with _ ⇒ constr_eq_nounivs a b end.
Ltac find_hyp T :=
  lazymatch T with
  | T
    ⇒
      multimatch goal with
      | [ H : T |- _ ] ⇒ H
      end
  | _
    ⇒
      multimatch goal with
      | [ H : ?T' |- _ ] ⇒ let __ := find_hyp_eq T T' in
                            H
      end
  end.

Ltac find_hyp_with_body body :=
  lazymatch body with
  | body
    ⇒
      multimatch goal with
      | [ H := body |- _ ] ⇒ H
      end
  | _
    ⇒
      multimatch goal with
      | [ H := ?body' |- _ ] ⇒ let __ := find_hyp_eq body body' in
                                H
      end
  end.