fact: Definition find_hyp {A:Type} : mlist Hyp -> t A := mfix1 f (l : mlist Hyp) : M A := match l with | (@ahyp A' x d) :m: l' => ou <- unify A' A UniEvarconv; match ou return t A with | mSome e => match e in _ =m= x return t x with meq_refl => M.ret x end | mNone => f l' end | _ => M.raise NotFound end.
imports: Strings.String NArith.BinNat Mtac2(Logic Datatypes Logic List Utils MTele Pattern Specif)