fact: Definition MTele_of {A:Type} (T : A -> Prop) : M (A -> msigT MTele_Ty) := M.nu (FreshFrom T) mNone (fun a => let T' := reduce (RedOneStep [rl:RedBeta]) (T a) in (mfix1 f (T : Prop) : M (msigT MTele_Ty) := mmatch T return M (msigT MTele_Ty) with | [?X : Type] M X =u> M.ret (mexistT _ mBase X) | [?(X : Type) (F : forall x:X, Prop)] (forall x:X, F x) =u> M.nu (FreshFrom T) mNone (fun x => let T' := reduce (RedOneStep [rl:RedBeta]) (F x) in '(mexistT _ n T) <- f T'; n' <- M.abs_fun x n; T' <- (M.coerce (B:=MTele_Ty (n' x)) T >>= M.abs_fun x); M.ret (mexistT _ (mTele n') T') ) end ) (T') >>= (fun t => t' <- M.abs_fun a t; M.ret t')).
imports: Coq.Strings.String Mtac2(Base Specif Logic Datatypes MTele MTeleMatchDef)