fact: Definition MTele_of : Prop -> M (sigT MTele_Ty) := mfix1 f (T : Prop) : M (sigT MTele_Ty) := mmatch T return M (sigT MTele_Ty) with | [?X : Type] M X =u> M.ret (existT _ mBase X) | [?(X : Type) (F : forall x:X, Prop)] (forall x:X, F x) =c> M.nu (FreshFrom F) mNone (fun x => '(existT _ n T) <- f (F x); n' <- M.abs_fun (P:=fun _ => MTele) x n; T' <- M.abs_fun x T; T' <- M.coerce T'; M.ret (existT _ (mTele n') T') ) end .
imports: Mtac2(Base Logic Datatypes MFixDef MTele MTeleMatch)