fact: Fixpoint branch_of_CTele {isort} {rsort} {it : ITele isort} (rt : RTele rsort it) (ct : CTele it) : stype_of rsort := match ct with | cBase a t => RTele_App a rt t | cProd f => ForAll (fun t => branch_of_CTele rt (f t)) end.
imports: Mtac2(Logic Datatypes List Sorts Base MTeleMatch MFix) Mtac2.tactics(Tactics ImportedTactics) Strings.String