-C).(\lambda (u: T).(arity g d u (asucc g (ASort O n))))))) H2))))) (\lambda
-(c0: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i0: nat).(\lambda (H1:
-(getl i0 c0 (CHead d (Bind Abbr) u))).(\lambda (a0: A).(\lambda (H2: (arity g
-d u a0)).(\lambda (_: (((eq T u (TLRef i)) \to (or (ex2_2 C T (\lambda (d0:
-C).(\lambda (u0: T).(getl i d (CHead d0 (Bind Abbr) u0)))) (\lambda (d0:
-C).(\lambda (u0: T).(arity g d0 u0 a0)))) (ex2_2 C T (\lambda (d0:
-C).(\lambda (u0: T).(getl i d (CHead d0 (Bind Abst) u0)))) (\lambda (d0:
-C).(\lambda (u0: T).(arity g d0 u0 (asucc g a0))))))))).(\lambda (H4: (eq T
-(TLRef i0) (TLRef i))).(let H5 \def (f_equal T nat (\lambda (e: T).(match e
-in T return (\lambda (_: T).nat) with [(TSort _) \Rightarrow i0 | (TLRef n)
-\Rightarrow n | (THead _ _ _) \Rightarrow i0])) (TLRef i0) (TLRef i) H4) in
-(let H6 \def (eq_ind nat i0 (\lambda (n: nat).(getl n c0 (CHead d (Bind Abbr)
-u))) H1 i H5) in (or_introl (ex2_2 C T (\lambda (d0: C).(\lambda (u0:
-T).(getl i c0 (CHead d0 (Bind Abbr) u0)))) (\lambda (d0: C).(\lambda (u0:
-T).(arity g d0 u0 a0)))) (ex2_2 C T (\lambda (d0: C).(\lambda (u0: T).(getl i
-c0 (CHead d0 (Bind Abst) u0)))) (\lambda (d0: C).(\lambda (u0: T).(arity g d0
-u0 (asucc g a0))))) (ex2_2_intro C T (\lambda (d0: C).(\lambda (u0: T).(getl
-i c0 (CHead d0 (Bind Abbr) u0)))) (\lambda (d0: C).(\lambda (u0: T).(arity g
-d0 u0 a0))) d u H6 H2))))))))))))) (\lambda (c0: C).(\lambda (d: C).(\lambda
-(u: T).(\lambda (i0: nat).(\lambda (H1: (getl i0 c0 (CHead d (Bind Abst)
-u))).(\lambda (a0: A).(\lambda (H2: (arity g d u (asucc g a0))).(\lambda (_:
-(((eq T u (TLRef i)) \to (or (ex2_2 C T (\lambda (d0: C).(\lambda (u0:
-T).(getl i d (CHead d0 (Bind Abbr) u0)))) (\lambda (d0: C).(\lambda (u0:
-T).(arity g d0 u0 (asucc g a0))))) (ex2_2 C T (\lambda (d0: C).(\lambda (u0:
-T).(getl i d (CHead d0 (Bind Abst) u0)))) (\lambda (d0: C).(\lambda (u0:
-T).(arity g d0 u0 (asucc g (asucc g a0)))))))))).(\lambda (H4: (eq T (TLRef
-i0) (TLRef i))).(let H5 \def (f_equal T nat (\lambda (e: T).(match e in T
-return (\lambda (_: T).nat) with [(TSort _) \Rightarrow i0 | (TLRef n)
-\Rightarrow n | (THead _ _ _) \Rightarrow i0])) (TLRef i0) (TLRef i) H4) in
-(let H6 \def (eq_ind nat i0 (\lambda (n: nat).(getl n c0 (CHead d (Bind Abst)
-u))) H1 i H5) in (or_intror (ex2_2 C T (\lambda (d0: C).(\lambda (u0:
-T).(getl i c0 (CHead d0 (Bind Abbr) u0)))) (\lambda (d0: C).(\lambda (u0:
-T).(arity g d0 u0 a0)))) (ex2_2 C T (\lambda (d0: C).(\lambda (u0: T).(getl i
-c0 (CHead d0 (Bind Abst) u0)))) (\lambda (d0: C).(\lambda (u0: T).(arity g d0
-u0 (asucc g a0))))) (ex2_2_intro C T (\lambda (d0: C).(\lambda (u0: T).(getl
-i c0 (CHead d0 (Bind Abst) u0)))) (\lambda (d0: C).(\lambda (u0: T).(arity g
-d0 u0 (asucc g a0)))) d u H6 H2))))))))))))) (\lambda (b: B).(\lambda (_:
-(not (eq B b Abst))).(\lambda (c0: C).(\lambda (u: T).(\lambda (a1:
-A).(\lambda (_: (arity g c0 u a1)).(\lambda (_: (((eq T u (TLRef i)) \to (or
-(ex2_2 C T (\lambda (d: C).(\lambda (u0: T).(getl i c0 (CHead d (Bind Abbr)
-u0)))) (\lambda (d: C).(\lambda (u0: T).(arity g d u0 a1)))) (ex2_2 C T
-(\lambda (d: C).(\lambda (u0: T).(getl i c0 (CHead d (Bind Abst) u0))))
-(\lambda (d: C).(\lambda (u0: T).(arity g d u0 (asucc g a1))))))))).(\lambda
-(t: T).(\lambda (a2: A).(\lambda (_: (arity g (CHead c0 (Bind b) u) t
-a2)).(\lambda (_: (((eq T t (TLRef i)) \to (or (ex2_2 C T (\lambda (d:
-C).(\lambda (u0: T).(getl i (CHead c0 (Bind b) u) (CHead d (Bind Abbr) u0))))
-(\lambda (d: C).(\lambda (u0: T).(arity g d u0 a2)))) (ex2_2 C T (\lambda (d:
-C).(\lambda (u0: T).(getl i (CHead c0 (Bind b) u) (CHead d (Bind Abst) u0))))
-(\lambda (d: C).(\lambda (u0: T).(arity g d u0 (asucc g a2))))))))).(\lambda
-(H6: (eq T (THead (Bind b) u t) (TLRef i))).(let H7 \def (eq_ind T (THead
-(Bind b) u t) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop)
-with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _
-_) \Rightarrow True])) I (TLRef i) H6) in (False_ind (or (ex2_2 C T (\lambda
-(d: C).(\lambda (u0: T).(getl i c0 (CHead d (Bind Abbr) u0)))) (\lambda (d:
-C).(\lambda (u0: T).(arity g d u0 a2)))) (ex2_2 C T (\lambda (d: C).(\lambda
-(u0: T).(getl i c0 (CHead d (Bind Abst) u0)))) (\lambda (d: C).(\lambda (u0:
-T).(arity g d u0 (asucc g a2)))))) H7)))))))))))))) (\lambda (c0: C).(\lambda
-(u: T).(\lambda (a1: A).(\lambda (_: (arity g c0 u (asucc g a1))).(\lambda
-(_: (((eq T u (TLRef i)) \to (or (ex2_2 C T (\lambda (d: C).(\lambda (u0:
-T).(getl i c0 (CHead d (Bind Abbr) u0)))) (\lambda (d: C).(\lambda (u0:
-T).(arity g d u0 (asucc g a1))))) (ex2_2 C T (\lambda (d: C).(\lambda (u0:
-T).(getl i c0 (CHead d (Bind Abst) u0)))) (\lambda (d: C).(\lambda (u0:
-T).(arity g d u0 (asucc g (asucc g a1)))))))))).(\lambda (t: T).(\lambda (a2:
-A).(\lambda (_: (arity g (CHead c0 (Bind Abst) u) t a2)).(\lambda (_: (((eq T
-t (TLRef i)) \to (or (ex2_2 C T (\lambda (d: C).(\lambda (u0: T).(getl i
-(CHead c0 (Bind Abst) u) (CHead d (Bind Abbr) u0)))) (\lambda (d: C).(\lambda
-(u0: T).(arity g d u0 a2)))) (ex2_2 C T (\lambda (d: C).(\lambda (u0:
-T).(getl i (CHead c0 (Bind Abst) u) (CHead d (Bind Abst) u0)))) (\lambda (d:
-C).(\lambda (u0: T).(arity g d u0 (asucc g a2))))))))).(\lambda (H5: (eq T
-(THead (Bind Abst) u t) (TLRef i))).(let H6 \def (eq_ind T (THead (Bind Abst)
-u t) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with
-[(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _)
-\Rightarrow True])) I (TLRef i) H5) in (False_ind (or (ex2_2 C T (\lambda (d:
-C).(\lambda (u0: T).(getl i c0 (CHead d (Bind Abbr) u0)))) (\lambda (d:
-C).(\lambda (u0: T).(arity g d u0 (AHead a1 a2))))) (ex2_2 C T (\lambda (d:
-C).(\lambda (u0: T).(getl i c0 (CHead d (Bind Abst) u0)))) (\lambda (d:
-C).(\lambda (u0: T).(arity g d u0 (asucc g (AHead a1 a2))))))) H6))))))))))))
-(\lambda (c0: C).(\lambda (u: T).(\lambda (a1: A).(\lambda (_: (arity g c0 u
+C).(\lambda (u: T).(arity g d u (asucc g a0)))))))))) (\lambda (c0:
+C).(\lambda (n: nat).(\lambda (H1: (eq T (TSort n) (TLRef i))).(let H2 \def
+(eq_ind T (TSort n) (\lambda (ee: T).(match ee in T return (\lambda (_:
+T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False |
+(THead _ _ _) \Rightarrow False])) I (TLRef i) H1) in (False_ind (or (ex2_2 C
+T (\lambda (d: C).(\lambda (u: T).(getl i c0 (CHead d (Bind Abbr) u))))
+(\lambda (d: C).(\lambda (u: T).(arity g d u (ASort O n))))) (ex2_2 C T
+(\lambda (d: C).(\lambda (u: T).(getl i c0 (CHead d (Bind Abst) u))))
+(\lambda (d: C).(\lambda (u: T).(arity g d u (asucc g (ASort O n)))))))
+H2))))) (\lambda (c0: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i0:
+nat).(\lambda (H1: (getl i0 c0 (CHead d (Bind Abbr) u))).(\lambda (a0:
+A).(\lambda (H2: (arity g d u a0)).(\lambda (_: (((eq T u (TLRef i)) \to (or
+(ex2_2 C T (\lambda (d0: C).(\lambda (u0: T).(getl i d (CHead d0 (Bind Abbr)
+u0)))) (\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0 a0)))) (ex2_2 C T
+(\lambda (d0: C).(\lambda (u0: T).(getl i d (CHead d0 (Bind Abst) u0))))
+(\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0 (asucc g
+a0))))))))).(\lambda (H4: (eq T (TLRef i0) (TLRef i))).(let H5 \def (f_equal
+T nat (\lambda (e: T).(match e in T return (\lambda (_: T).nat) with [(TSort
+_) \Rightarrow i0 | (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow i0]))
+(TLRef i0) (TLRef i) H4) in (let H6 \def (eq_ind nat i0 (\lambda (n:
+nat).(getl n c0 (CHead d (Bind Abbr) u))) H1 i H5) in (or_introl (ex2_2 C T
+(\lambda (d0: C).(\lambda (u0: T).(getl i c0 (CHead d0 (Bind Abbr) u0))))
+(\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0 a0)))) (ex2_2 C T (\lambda
+(d0: C).(\lambda (u0: T).(getl i c0 (CHead d0 (Bind Abst) u0)))) (\lambda
+(d0: C).(\lambda (u0: T).(arity g d0 u0 (asucc g a0))))) (ex2_2_intro C T
+(\lambda (d0: C).(\lambda (u0: T).(getl i c0 (CHead d0 (Bind Abbr) u0))))
+(\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0 a0))) d u H6 H2)))))))))))))
+(\lambda (c0: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i0: nat).(\lambda
+(H1: (getl i0 c0 (CHead d (Bind Abst) u))).(\lambda (a0: A).(\lambda (H2:
+(arity g d u (asucc g a0))).(\lambda (_: (((eq T u (TLRef i)) \to (or (ex2_2
+C T (\lambda (d0: C).(\lambda (u0: T).(getl i d (CHead d0 (Bind Abbr) u0))))
+(\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0 (asucc g a0))))) (ex2_2 C T
+(\lambda (d0: C).(\lambda (u0: T).(getl i d (CHead d0 (Bind Abst) u0))))
+(\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0 (asucc g (asucc g
+a0)))))))))).(\lambda (H4: (eq T (TLRef i0) (TLRef i))).(let H5 \def (f_equal
+T nat (\lambda (e: T).(match e in T return (\lambda (_: T).nat) with [(TSort
+_) \Rightarrow i0 | (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow i0]))
+(TLRef i0) (TLRef i) H4) in (let H6 \def (eq_ind nat i0 (\lambda (n:
+nat).(getl n c0 (CHead d (Bind Abst) u))) H1 i H5) in (or_intror (ex2_2 C T
+(\lambda (d0: C).(\lambda (u0: T).(getl i c0 (CHead d0 (Bind Abbr) u0))))
+(\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0 a0)))) (ex2_2 C T (\lambda
+(d0: C).(\lambda (u0: T).(getl i c0 (CHead d0 (Bind Abst) u0)))) (\lambda
+(d0: C).(\lambda (u0: T).(arity g d0 u0 (asucc g a0))))) (ex2_2_intro C T
+(\lambda (d0: C).(\lambda (u0: T).(getl i c0 (CHead d0 (Bind Abst) u0))))
+(\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0 (asucc g a0)))) d u H6
+H2))))))))))))) (\lambda (b: B).(\lambda (_: (not (eq B b Abst))).(\lambda
+(c0: C).(\lambda (u: T).(\lambda (a1: A).(\lambda (_: (arity g c0 u