fact: Definition apply_param_constr {s} {i : ITele s} : forall (a : ATele i) (c : CTele i), M (CTele (mprojT1 (apply_arg i a))) := match i as i return forall (a : ATele i) (c : CTele i), M (CTele (mprojT1 (apply_arg i a))) with | iBase _ => fun _ c => M.ret c | iTele f => fun '(existT _ arg args as at1) => (fix go first (c : CTele (iTele f)) : M (CTele (f arg)) := match c , first with | cBase (existT _ arg' args' as at2) app, false => mmatch arg as arg return M (CTele (f arg)) with | arg' =u> let app := match eq_sym (ITele_App_eq (i:=iTele f) at2) in _ = x return x with | eq_refl => app end in M.ret (cBase args' app) end | cBase _ _, true => M.failwith "constructor takes no more arguments." | cProd F, true => let A := _ in let B := _ in arg <- @M.coerce A B arg; c <- go false (F arg); M.ret c | cProd F, false => \nu x, c <- go false (F x); c <- M.abs_fun x c; M.ret (cProd c) end) true end.
imports: Mtac2(Logic Datatypes List Sorts Base MTeleMatch MFix) Mtac2.tactics(Tactics ImportedTactics) Strings.String Mtac2.lib.Specif