fact: Definition copy_ctx {A} (B : A -> Type) : dyn -> M Type := mfix1 rec (d : dyn) : M Type := mmatch d with | [? c : A] Dyn c => let Bc := reduce (RedWhd [rl:RedBeta]) (B c) in M.ret Bc | [? C (D : C -> Type) (c : forall y:C, D y)] Dyn c => M.nu (FreshFrom c) mNone (fun y=> r <- rec (Dyn (c y)); M.abs_prod_type y r) | [? C D (c : C->D)] Dyn c => M.nu (FreshFrom c) mNone (fun y=> r <- rec (Dyn (c y)); M.abs_prod_type y r) | _ => M.print_term A;; M.raise (SomethingNotRight d) end.
imports: Strings.String ssrmatching.ssrmatching Mtac2(Logic Datatypes List Utils Logic Sorts MTeleMatch) Strings.String NArith.BinNat NArith.BinNatDef