fact: Definition MTele_of' := (mfix1 f (T : Prop) : M { m : MTele & { mT : MTele_Ty m & T =m= MFA mT } } := (mtmmatch T as T0 return T =m= T0 -> M { m : MTele & { mT : MTele_Ty m & T =m= MFA mT } } with | [?X : Type] M X =u> fun H => M.ret (existT (fun m => {mT : MTele_Ty m & T =m= MFA mT}) (mBase) (existT (fun mT : MTele_Ty mBase => T =m= MFA mT) _ H) ) | [?(X : Type) (F : forall x:X, Prop)] (forall x:X, F x) =c> fun H => M.nu (FreshFrom F) mNone (fun x => '(existT _ m (existT _ mT E)) <- f (F x); m' <- M.abs_fun x m; mT' <- (M.coerce mT >>= M.abs_fun (P:=fun x => MTele_Ty (m' x)) x); E' <- M.coerce (@meq_refl _ (MFA (n:=mTele m') mT')); M.ret (existT _ (mTele m') (existT _ mT' E')) ) end) meq_refl ).
imports: Mtac2(Base Logic Datatypes MFixDef MTele MTeleMatch)