fact: Definition inst_evar {A} (x y : A) : t (moption (x =m= y)) := instantiate_evar (P:=fun t => moption (t =m= y)) x y (M.ret (mSome meq_refl)) (M.ret mNone).
imports: Strings.String NArith.BinNat Mtac2(Logic Datatypes Logic List Utils MTele Pattern Specif)