fact: Definition branch_of_NDCTele {isort} {rsort} {it : ITele isort} (rt : RTele rsort it) (ct : NDCTele it) : stype_of rsort := (fix rec l := match l as l' return NDCfold it l' -> rsort with | [m:] => fun f => RTele_App (projT1 (f tt)) rt (projT2 (f tt)) | T :m: l => fun f => ForAll (fun t : T => rec l (fun y => f(m: t,y))) end) (projT1 ct) (projT2 ct).
imports: Mtac2(Logic Datatypes List Sorts Base MTeleMatch MFix) Mtac2.tactics(Tactics ImportedTactics) Strings.String