fact: Fixpoint apply_args {s} (i : ITele s) (a : ATele i) (n : nat) : msigT ATele := match n with | 0 => mexistT ATele i a | S n => let '(mexistT _ it args) := apply_arg i a in apply_args it args n end.
imports: Mtac2(Logic Datatypes List Sorts Base MTeleMatch MFix) Mtac2.tactics(Tactics ImportedTactics) Strings.String Mtac2.lib.Specif