fact: Definition apply_type_of (P : Type) : forall {T} (t : T), M (sigT (funs_of (M P))) := mfix f (T : _) : T -> M (sigT (funs_of (M P))) := mtmmatch T as T' return T' -> M (sigT (funs_of (M P))) with | (M P : Type) =c> fun t => M.ret (existT (funs_of (M P)) [m:] t) | [? X F] (forall x : X, F x) =c> fun ft => M.nu (FreshFrom ft) mNone (fun x_nu : X => x <- M.evar X; let F' := reduce (RedOneStep [rl:RedBeta]) (F x) in let f' := reduce (RedOneStep [rl:RedBeta]) (ft x) in r <- f F' f'; mif M.is_evar x then o <- M.unify x_nu x UniEvarconv; let '(existT _ rl rp) := r in rp' <- M.abs_fun x_nu rp; mtry (M.remove x_nu ( let r' : sigT (funs_of (M P)) := existT _ (M X :m: rl) (funs_bind rp') in M.ret r' )) with | [?s] CannotRemoveVar s => let err := (String.append "A hypothesis depends on " s) in M.failwith err end else M.remove x_nu (M.ret r) ) | _ as _catchall => fun _ => M.failwith "The lemma's conclusion does not unify with the goal." end .
imports: Coq.Strings.String Mtac2(Base Logic Datatypes List MFix MTeleMatch)