fact: Definition mwith {A B} (c : A) (n : string) (v : B) : t dyn := (mfix1 app (d : dyn) : M _ := dcase d as ty, el in mmatch d return t dyn with | [? T1 T2 f] @Dyn (forall x:T1, T2 x) f => let ty := reduce (RedWhd [rl:RedBeta]) ty in binder <- get_binder_name ty; mif unify binder n UniMatchNoRed then oeq' <- unify B T1 UniCoq; match oeq' with | mSome eq' => let v' := reduce (RedWhd [rl:RedMatch]) match eq' as x in _ =m= x with meq_refl=> v end in ret (Dyn (f v')) | _ => raise (WrongType T1) end else e <- evar T1; app (Dyn (f e)) | _ => raise (NameNotFound n) end ) (Dyn c).
imports: Strings.String NArith.BinNat Mtac2(Logic Datatypes Logic List Utils MTele Pattern Specif)