fact: Fixpoint apply_params_constrs {s} {i : ITele s} (n : nat) : forall (args : ATele i) (cs : mlist (CTele i)), M (mlist (CTele (mprojT1 (apply_args i args n)))) := let P := (fun i : ITele s => ATele i *m mlist (CTele i)) in match n, i as i return forall (args : ATele i) (cs : mlist (CTele i)), M (mlist (CTele (mprojT1 (apply_args i args n)))) with | 0, _ => fun a cs => M.ret cs | S m, iTele f => fun '(existT _ a args as args') cs => cs <- M.map (apply_param_constr (i:=iTele f) args') cs; apply_params_constrs m _ cs | S m, iBase _ => fun _ _ => M.failwith "Reached iBase but am supposed to apply more parameters" end .
imports: Mtac2(Logic Datatypes List Sorts Base MTeleMatch MFix) Mtac2.tactics(Tactics ImportedTactics) Strings.String Mtac2.lib.Specif