fact: Definition find_hyp_index {A} (x : A) : t (moption nat) := index_of (fun y => mmatch y with | [? b] ahyp x b => M.ret true | _ => ret false end) =<< M.hyps.
imports: Strings.String NArith.BinNat Mtac2(Logic Datatypes Logic List Utils MTele Pattern Specif)