fact: Fixpoint ITele_App {isort} {it : ITele isort} : forall (args : ATele it), isort := match it with | iBase T => fun _ => T | iTele f => fun '(existT _ t a) => ITele_App a end.
imports: Mtac2(Logic Datatypes List Sorts Base MTeleMatch MFix) Mtac2.tactics(Tactics ImportedTactics) Strings.String