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