X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Farity%2Ffwd.ma;h=0c815117490c4a4b6c73d84da6887a614c0342f1;hb=6329f0f87906d3347c39d2ba2f5ec2b2124f17a2;hp=e2a3e07928a67bc5c944e94134d06157f84163c5;hpb=783fbc6eb42d5db260d93d8d213a7d5c035e99e3;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/fwd.ma
index e2a3e0792..0c8151174 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/fwd.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-
+set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/fwd".
 
 include "arity/defs.ma".
 
@@ -30,35 +30,35 @@ theorem arity_gen_sort:
 \def
  \lambda (g: G).(\lambda (c: C).(\lambda (n: nat).(\lambda (a: A).(\lambda 
 (H: (arity g c (TSort n) a)).(insert_eq T (TSort n) (\lambda (t: T).(arity g 
-c t a)) (leq g a (ASort O n)) (\lambda (y: T).(\lambda (H0: (arity g c y 
-a)).(arity_ind g (\lambda (_: C).(\lambda (t: T).(\lambda (a0: A).((eq T t 
-(TSort n)) \to (leq g a0 (ASort O n)))))) (\lambda (_: C).(\lambda (n0: 
-nat).(\lambda (H1: (eq T (TSort n0) (TSort n))).(let H2 \def (f_equal T nat 
-(\lambda (e: T).(match e in T return (\lambda (_: T).nat) with [(TSort n1) 
-\Rightarrow n1 | (TLRef _) \Rightarrow n0 | (THead _ _ _) \Rightarrow n0])) 
-(TSort n0) (TSort n) H1) in (eq_ind_r nat n (\lambda (n1: nat).(leq g (ASort 
-O n1) (ASort O n))) (leq_refl g (ASort O n)) n0 H2))))) (\lambda (c0: 
-C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda (_: (getl i c0 
-(CHead d (Bind Abbr) u))).(\lambda (a0: A).(\lambda (_: (arity g d u 
-a0)).(\lambda (_: (((eq T u (TSort n)) \to (leq g a0 (ASort O n))))).(\lambda 
-(H4: (eq T (TLRef i) (TSort n))).(let H5 \def (eq_ind T (TLRef i) (\lambda 
-(ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) 
-\Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow 
-False])) I (TSort n) H4) in (False_ind (leq g a0 (ASort O n)) H5))))))))))) 
+c t a)) (\lambda (_: T).(leq g a (ASort O n))) (\lambda (y: T).(\lambda (H0: 
+(arity g c y a)).(arity_ind g (\lambda (_: C).(\lambda (t: T).(\lambda (a0: 
+A).((eq T t (TSort n)) \to (leq g a0 (ASort O n)))))) (\lambda (_: 
+C).(\lambda (n0: nat).(\lambda (H1: (eq T (TSort n0) (TSort n))).(let H2 \def 
+(f_equal T nat (\lambda (e: T).(match e in T return (\lambda (_: T).nat) with 
+[(TSort n1) \Rightarrow n1 | (TLRef _) \Rightarrow n0 | (THead _ _ _) 
+\Rightarrow n0])) (TSort n0) (TSort n) H1) in (eq_ind_r nat n (\lambda (n1: 
+nat).(leq g (ASort O n1) (ASort O n))) (leq_refl g (ASort O n)) n0 H2))))) 
 (\lambda (c0: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda 
-(_: (getl i c0 (CHead d (Bind Abst) u))).(\lambda (a0: A).(\lambda (_: (arity 
-g d u (asucc g a0))).(\lambda (_: (((eq T u (TSort n)) \to (leq g (asucc g 
-a0) (ASort O n))))).(\lambda (H4: (eq T (TLRef i) (TSort n))).(let H5 \def 
-(eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T return (\lambda (_: 
-T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | 
-(THead _ _ _) \Rightarrow False])) I (TSort n) H4) in (False_ind (leq g a0 
-(ASort O n)) H5))))))))))) (\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 (TSort n)) \to (leq g a1 (ASort O 
-n))))).(\lambda (t: T).(\lambda (a2: A).(\lambda (_: (arity g (CHead c0 (Bind 
-b) u) t a2)).(\lambda (_: (((eq T t (TSort n)) \to (leq g a2 (ASort O 
-n))))).(\lambda (H6: (eq T (THead (Bind b) u t) (TSort n))).(let H7 \def 
-(eq_ind T (THead (Bind b) u t) (\lambda (ee: T).(match ee in T return 
+(_: (getl i c0 (CHead d (Bind Abbr) u))).(\lambda (a0: A).(\lambda (_: (arity 
+g d u a0)).(\lambda (_: (((eq T u (TSort n)) \to (leq g a0 (ASort O 
+n))))).(\lambda (H4: (eq T (TLRef i) (TSort n))).(let H5 \def (eq_ind T 
+(TLRef i) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with 
+[(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) 
+\Rightarrow False])) I (TSort n) H4) in (False_ind (leq g a0 (ASort O n)) 
+H5))))))))))) (\lambda (c0: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: 
+nat).(\lambda (_: (getl i c0 (CHead d (Bind Abst) u))).(\lambda (a0: 
+A).(\lambda (_: (arity g d u (asucc g a0))).(\lambda (_: (((eq T u (TSort n)) 
+\to (leq g (asucc g a0) (ASort O n))))).(\lambda (H4: (eq T (TLRef i) (TSort 
+n))).(let H5 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T return 
+(\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) 
+\Rightarrow True | (THead _ _ _) \Rightarrow False])) I (TSort n) H4) in 
+(False_ind (leq g a0 (ASort O n)) H5))))))))))) (\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 (TSort n)) \to (leq 
+g a1 (ASort O n))))).(\lambda (t: T).(\lambda (a2: A).(\lambda (_: (arity g 
+(CHead c0 (Bind b) u) t a2)).(\lambda (_: (((eq T t (TSort n)) \to (leq g a2 
+(ASort O n))))).(\lambda (H6: (eq T (THead (Bind b) u t) (TSort n))).(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 (TSort n) H6) in 
 (False_ind (leq g a2 (ASort O n)) H7)))))))))))))) (\lambda (c0: C).(\lambda 
@@ -106,114 +106,115 @@ u)))) (\lambda (d: C).(\lambda (u: T).(arity g d u (asucc g a))))))))))
 \def
  \lambda (g: G).(\lambda (c: C).(\lambda (i: nat).(\lambda (a: A).(\lambda 
 (H: (arity g c (TLRef i) a)).(insert_eq T (TLRef i) (\lambda (t: T).(arity g 
-c t a)) (or (ex2_2 C T (\lambda (d: C).(\lambda (u: T).(getl i c (CHead d 
-(Bind Abbr) u)))) (\lambda (d: C).(\lambda (u: T).(arity g d u a)))) (ex2_2 C 
-T (\lambda (d: C).(\lambda (u: T).(getl i c (CHead d (Bind Abst) u)))) 
-(\lambda (d: C).(\lambda (u: T).(arity g d u (asucc g a)))))) (\lambda (y: 
-T).(\lambda (H0: (arity g c y a)).(arity_ind g (\lambda (c0: C).(\lambda (t: 
-T).(\lambda (a0: A).((eq T t (TLRef i)) \to (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 a0)))) (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 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 t a)) (\lambda (_: T).(or (ex2_2 C T (\lambda (d: C).(\lambda (u: T).(getl 
+i c (CHead d (Bind Abbr) u)))) (\lambda (d: C).(\lambda (u: T).(arity g d u 
+a)))) (ex2_2 C T (\lambda (d: C).(\lambda (u: T).(getl i c (CHead d (Bind 
+Abst) u)))) (\lambda (d: C).(\lambda (u: T).(arity g d u (asucc g a))))))) 
+(\lambda (y: T).(\lambda (H0: (arity g c y a)).(arity_ind g (\lambda (c0: 
+C).(\lambda (t: T).(\lambda (a0: A).((eq T t (TLRef i)) \to (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 a0)))) (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 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 
 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 c0 t (AHead a1 a2))).(\lambda (_: (((eq T t (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 (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)))))))))).(\lambda (H5: (eq T (THead (Flat Appl) u t) (TLRef i))).(let 
-H6 \def (eq_ind T (THead (Flat Appl) u t) (\lambda (ee: T).(match ee in T 
-return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) 
+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 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 
+c0 t (AHead a1 a2))).(\lambda (_: (((eq T t (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 (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)))))))))).(\lambda (H5: (eq T (THead (Flat Appl) u t) (TLRef i))).(let H6 
+\def (eq_ind T (THead (Flat Appl) 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 a2)))) 
@@ -303,21 +304,21 @@ A).(arity g (CHead c (Bind b) u) t a2))))))))))
  \lambda (b: B).(\lambda (H: (not (eq B b Abst))).(\lambda (g: G).(\lambda 
 (c: C).(\lambda (u: T).(\lambda (t: T).(\lambda (a2: A).(\lambda (H0: (arity 
 g c (THead (Bind b) u t) a2)).(insert_eq T (THead (Bind b) u t) (\lambda (t0: 
-T).(arity g c t0 a2)) (ex2 A (\lambda (a1: A).(arity g c u a1)) (\lambda (_: 
-A).(arity g (CHead c (Bind b) u) t a2))) (\lambda (y: T).(\lambda (H1: (arity 
-g c y a2)).(arity_ind g (\lambda (c0: C).(\lambda (t0: T).(\lambda (a: 
-A).((eq T t0 (THead (Bind b) u t)) \to (ex2 A (\lambda (a1: A).(arity g c0 u 
-a1)) (\lambda (_: A).(arity g (CHead c0 (Bind b) u) t a))))))) (\lambda (c0: 
-C).(\lambda (n: nat).(\lambda (H2: (eq T (TSort n) (THead (Bind b) u 
-t))).(let H3 \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 (THead (Bind b) u t) 
-H2) in (False_ind (ex2 A (\lambda (a1: A).(arity g c0 u a1)) (\lambda (_: 
-A).(arity g (CHead c0 (Bind b) u) t (ASort O n)))) H3))))) (\lambda (c0: 
-C).(\lambda (d: C).(\lambda (u0: T).(\lambda (i: nat).(\lambda (_: (getl i c0 
-(CHead d (Bind Abbr) u0))).(\lambda (a: A).(\lambda (_: (arity g d u0 
-a)).(\lambda (_: (((eq T u0 (THead (Bind b) u t)) \to (ex2 A (\lambda (a1: 
-A).(arity g d u a1)) (\lambda (_: A).(arity g (CHead d (Bind b) u) t 
+T).(arity g c t0 a2)) (\lambda (_: T).(ex2 A (\lambda (a1: A).(arity g c u 
+a1)) (\lambda (_: A).(arity g (CHead c (Bind b) u) t a2)))) (\lambda (y: 
+T).(\lambda (H1: (arity g c y a2)).(arity_ind g (\lambda (c0: C).(\lambda 
+(t0: T).(\lambda (a: A).((eq T t0 (THead (Bind b) u t)) \to (ex2 A (\lambda 
+(a1: A).(arity g c0 u a1)) (\lambda (_: A).(arity g (CHead c0 (Bind b) u) t 
+a))))))) (\lambda (c0: C).(\lambda (n: nat).(\lambda (H2: (eq T (TSort n) 
+(THead (Bind b) u t))).(let H3 \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 
+(THead (Bind b) u t) H2) in (False_ind (ex2 A (\lambda (a1: A).(arity g c0 u 
+a1)) (\lambda (_: A).(arity g (CHead c0 (Bind b) u) t (ASort O n)))) H3))))) 
+(\lambda (c0: C).(\lambda (d: C).(\lambda (u0: T).(\lambda (i: nat).(\lambda 
+(_: (getl i c0 (CHead d (Bind Abbr) u0))).(\lambda (a: A).(\lambda (_: (arity 
+g d u0 a)).(\lambda (_: (((eq T u0 (THead (Bind b) u t)) \to (ex2 A (\lambda 
+(a1: A).(arity g d u a1)) (\lambda (_: A).(arity g (CHead d (Bind b) u) t 
 a)))))).(\lambda (H5: (eq T (TLRef i) (THead (Bind b) u t))).(let H6 \def 
 (eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T return (\lambda (_: 
 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | 
@@ -472,215 +473,216 @@ A).(arity g c u (asucc g a1)))) (\lambda (_: A).(\lambda (a2: A).(arity g
 \def
  \lambda (g: G).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(\lambda (a: 
 A).(\lambda (H: (arity g c (THead (Bind Abst) u t) a)).(insert_eq T (THead 
-(Bind Abst) u t) (\lambda (t0: T).(arity g c t0 a)) (ex3_2 A A (\lambda (a1: 
-A).(\lambda (a2: A).(eq A a (AHead a1 a2)))) (\lambda (a1: A).(\lambda (_: 
-A).(arity g c u (asucc g a1)))) (\lambda (_: A).(\lambda (a2: A).(arity g 
-(CHead c (Bind Abst) u) t a2)))) (\lambda (y: T).(\lambda (H0: (arity g c y 
-a)).(arity_ind g (\lambda (c0: C).(\lambda (t0: T).(\lambda (a0: A).((eq T t0 
-(THead (Bind Abst) u t)) \to (ex3_2 A A (\lambda (a1: A).(\lambda (a2: A).(eq 
-A a0 (AHead a1 a2)))) (\lambda (a1: A).(\lambda (_: A).(arity g c0 u (asucc g 
+(Bind Abst) u t) (\lambda (t0: T).(arity g c t0 a)) (\lambda (_: T).(ex3_2 A 
+A (\lambda (a1: A).(\lambda (a2: A).(eq A a (AHead a1 a2)))) (\lambda (a1: 
+A).(\lambda (_: A).(arity g c u (asucc g a1)))) (\lambda (_: A).(\lambda (a2: 
+A).(arity g (CHead c (Bind Abst) u) t a2))))) (\lambda (y: T).(\lambda (H0: 
+(arity g c y a)).(arity_ind g (\lambda (c0: C).(\lambda (t0: T).(\lambda (a0: 
+A).((eq T t0 (THead (Bind Abst) u t)) \to (ex3_2 A A (\lambda (a1: 
+A).(\lambda (a2: A).(eq A a0 (AHead a1 a2)))) (\lambda (a1: A).(\lambda (_: 
+A).(arity g c0 u (asucc g a1)))) (\lambda (_: A).(\lambda (a2: A).(arity g 
+(CHead c0 (Bind Abst) u) t a2)))))))) (\lambda (c0: C).(\lambda (n: 
+nat).(\lambda (H1: (eq T (TSort n) (THead (Bind Abst) u t))).(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 (THead (Bind Abst) u t) H1) in 
+(False_ind (ex3_2 A A (\lambda (a1: A).(\lambda (a2: A).(eq A (ASort O n) 
+(AHead a1 a2)))) (\lambda (a1: A).(\lambda (_: A).(arity g c0 u (asucc g 
 a1)))) (\lambda (_: A).(\lambda (a2: A).(arity g (CHead c0 (Bind Abst) u) t 
-a2)))))))) (\lambda (c0: C).(\lambda (n: nat).(\lambda (H1: (eq T (TSort n) 
-(THead (Bind Abst) u t))).(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 
-(THead (Bind Abst) u t) H1) in (False_ind (ex3_2 A A (\lambda (a1: 
-A).(\lambda (a2: A).(eq A (ASort O n) (AHead a1 a2)))) (\lambda (a1: 
-A).(\lambda (_: A).(arity g c0 u (asucc g a1)))) (\lambda (_: A).(\lambda 
-(a2: A).(arity g (CHead c0 (Bind Abst) u) t a2)))) H2))))) (\lambda (c0: 
-C).(\lambda (d: C).(\lambda (u0: T).(\lambda (i: nat).(\lambda (_: (getl i c0 
-(CHead d (Bind Abbr) u0))).(\lambda (a0: A).(\lambda (_: (arity g d u0 
-a0)).(\lambda (_: (((eq T u0 (THead (Bind Abst) u t)) \to (ex3_2 A A (\lambda 
-(a1: A).(\lambda (a2: A).(eq A a0 (AHead a1 a2)))) (\lambda (a1: A).(\lambda 
-(_: A).(arity g d u (asucc g a1)))) (\lambda (_: A).(\lambda (a2: A).(arity g 
-(CHead d (Bind Abst) u) t a2))))))).(\lambda (H4: (eq T (TLRef i) (THead 
-(Bind Abst) u t))).(let H5 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match 
-ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | 
-(TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead 
-(Bind Abst) u t) H4) in (False_ind (ex3_2 A A (\lambda (a1: A).(\lambda (a2: 
-A).(eq A a0 (AHead a1 a2)))) (\lambda (a1: A).(\lambda (_: A).(arity g c0 u 
-(asucc g a1)))) (\lambda (_: A).(\lambda (a2: A).(arity g (CHead c0 (Bind 
-Abst) u) t a2)))) H5))))))))))) (\lambda (c0: C).(\lambda (d: C).(\lambda 
-(u0: T).(\lambda (i: nat).(\lambda (_: (getl i c0 (CHead d (Bind Abst) 
-u0))).(\lambda (a0: A).(\lambda (_: (arity g d u0 (asucc g a0))).(\lambda (_: 
-(((eq T u0 (THead (Bind Abst) u t)) \to (ex3_2 A A (\lambda (a1: A).(\lambda 
-(a2: A).(eq A (asucc g a0) (AHead a1 a2)))) (\lambda (a1: A).(\lambda (_: 
-A).(arity g d u (asucc g a1)))) (\lambda (_: A).(\lambda (a2: A).(arity g 
-(CHead d (Bind Abst) u) t a2))))))).(\lambda (H4: (eq T (TLRef i) (THead 
-(Bind Abst) u t))).(let H5 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match 
-ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | 
-(TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead 
-(Bind Abst) u t) H4) in (False_ind (ex3_2 A A (\lambda (a1: A).(\lambda (a2: 
-A).(eq A a0 (AHead a1 a2)))) (\lambda (a1: A).(\lambda (_: A).(arity g c0 u 
-(asucc g a1)))) (\lambda (_: A).(\lambda (a2: A).(arity g (CHead c0 (Bind 
-Abst) u) t a2)))) H5))))))))))) (\lambda (b: B).(\lambda (H1: (not (eq B b 
-Abst))).(\lambda (c0: C).(\lambda (u0: T).(\lambda (a1: A).(\lambda (H2: 
-(arity g c0 u0 a1)).(\lambda (H3: (((eq T u0 (THead (Bind Abst) u t)) \to 
-(ex3_2 A A (\lambda (a2: A).(\lambda (a3: A).(eq A a1 (AHead a2 a3)))) 
-(\lambda (a2: A).(\lambda (_: A).(arity g c0 u (asucc g a2)))) (\lambda (_: 
-A).(\lambda (a3: A).(arity g (CHead c0 (Bind Abst) u) t a3))))))).(\lambda 
-(t0: T).(\lambda (a2: A).(\lambda (H4: (arity g (CHead c0 (Bind b) u0) t0 
-a2)).(\lambda (H5: (((eq T t0 (THead (Bind Abst) u t)) \to (ex3_2 A A 
-(\lambda (a3: A).(\lambda (a4: A).(eq A a2 (AHead a3 a4)))) (\lambda (a3: 
-A).(\lambda (_: A).(arity g (CHead c0 (Bind b) u0) u (asucc g a3)))) (\lambda 
-(_: A).(\lambda (a4: A).(arity g (CHead (CHead c0 (Bind b) u0) (Bind Abst) u) 
-t a4))))))).(\lambda (H6: (eq T (THead (Bind b) u0 t0) (THead (Bind Abst) u 
-t))).(let H7 \def (f_equal T B (\lambda (e: T).(match e in T return (\lambda 
-(_: T).B) with [(TSort _) \Rightarrow b | (TLRef _) \Rightarrow b | (THead k 
-_ _) \Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b0) 
-\Rightarrow b0 | (Flat _) \Rightarrow b])])) (THead (Bind b) u0 t0) (THead 
-(Bind Abst) u t) H6) in ((let H8 \def (f_equal T T (\lambda (e: T).(match e 
-in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow u0 | (TLRef _) 
-\Rightarrow u0 | (THead _ t1 _) \Rightarrow t1])) (THead (Bind b) u0 t0) 
-(THead (Bind Abst) u t) H6) in ((let H9 \def (f_equal T T (\lambda (e: 
-T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t0 | 
-(TLRef _) \Rightarrow t0 | (THead _ _ t1) \Rightarrow t1])) (THead (Bind b) 
-u0 t0) (THead (Bind Abst) u t) H6) in (\lambda (H10: (eq T u0 u)).(\lambda 
-(H11: (eq B b Abst)).(let H12 \def (eq_ind T t0 (\lambda (t1: T).((eq T t1 
+a2)))) H2))))) (\lambda (c0: C).(\lambda (d: C).(\lambda (u0: T).(\lambda (i: 
+nat).(\lambda (_: (getl i c0 (CHead d (Bind Abbr) u0))).(\lambda (a0: 
+A).(\lambda (_: (arity g d u0 a0)).(\lambda (_: (((eq T u0 (THead (Bind Abst) 
+u t)) \to (ex3_2 A A (\lambda (a1: A).(\lambda (a2: A).(eq A a0 (AHead a1 
+a2)))) (\lambda (a1: A).(\lambda (_: A).(arity g d u (asucc g a1)))) (\lambda 
+(_: A).(\lambda (a2: A).(arity g (CHead d (Bind Abst) u) t a2))))))).(\lambda 
+(H4: (eq T (TLRef i) (THead (Bind Abst) u t))).(let H5 \def (eq_ind T (TLRef 
+i) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort 
+_) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow 
+False])) I (THead (Bind Abst) u t) H4) in (False_ind (ex3_2 A A (\lambda (a1: 
+A).(\lambda (a2: A).(eq A a0 (AHead a1 a2)))) (\lambda (a1: A).(\lambda (_: 
+A).(arity g c0 u (asucc g a1)))) (\lambda (_: A).(\lambda (a2: A).(arity g 
+(CHead c0 (Bind Abst) u) t a2)))) H5))))))))))) (\lambda (c0: C).(\lambda (d: 
+C).(\lambda (u0: T).(\lambda (i: nat).(\lambda (_: (getl i c0 (CHead d (Bind 
+Abst) u0))).(\lambda (a0: A).(\lambda (_: (arity g d u0 (asucc g 
+a0))).(\lambda (_: (((eq T u0 (THead (Bind Abst) u t)) \to (ex3_2 A A 
+(\lambda (a1: A).(\lambda (a2: A).(eq A (asucc g a0) (AHead a1 a2)))) 
+(\lambda (a1: A).(\lambda (_: A).(arity g d u (asucc g a1)))) (\lambda (_: 
+A).(\lambda (a2: A).(arity g (CHead d (Bind Abst) u) t a2))))))).(\lambda 
+(H4: (eq T (TLRef i) (THead (Bind Abst) u t))).(let H5 \def (eq_ind T (TLRef 
+i) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort 
+_) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow 
+False])) I (THead (Bind Abst) u t) H4) in (False_ind (ex3_2 A A (\lambda (a1: 
+A).(\lambda (a2: A).(eq A a0 (AHead a1 a2)))) (\lambda (a1: A).(\lambda (_: 
+A).(arity g c0 u (asucc g a1)))) (\lambda (_: A).(\lambda (a2: A).(arity g 
+(CHead c0 (Bind Abst) u) t a2)))) H5))))))))))) (\lambda (b: B).(\lambda (H1: 
+(not (eq B b Abst))).(\lambda (c0: C).(\lambda (u0: T).(\lambda (a1: 
+A).(\lambda (H2: (arity g c0 u0 a1)).(\lambda (H3: (((eq T u0 (THead (Bind 
+Abst) u t)) \to (ex3_2 A A (\lambda (a2: A).(\lambda (a3: A).(eq A a1 (AHead 
+a2 a3)))) (\lambda (a2: A).(\lambda (_: A).(arity g c0 u (asucc g a2)))) 
+(\lambda (_: A).(\lambda (a3: A).(arity g (CHead c0 (Bind Abst) u) t 
+a3))))))).(\lambda (t0: T).(\lambda (a2: A).(\lambda (H4: (arity g (CHead c0 
+(Bind b) u0) t0 a2)).(\lambda (H5: (((eq T t0 (THead (Bind Abst) u t)) \to 
+(ex3_2 A A (\lambda (a3: A).(\lambda (a4: A).(eq A a2 (AHead a3 a4)))) 
+(\lambda (a3: A).(\lambda (_: A).(arity g (CHead c0 (Bind b) u0) u (asucc g 
+a3)))) (\lambda (_: A).(\lambda (a4: A).(arity g (CHead (CHead c0 (Bind b) 
+u0) (Bind Abst) u) t a4))))))).(\lambda (H6: (eq T (THead (Bind b) u0 t0) 
+(THead (Bind Abst) u t))).(let H7 \def (f_equal T B (\lambda (e: T).(match e 
+in T return (\lambda (_: T).B) with [(TSort _) \Rightarrow b | (TLRef _) 
+\Rightarrow b | (THead k _ _) \Rightarrow (match k in K return (\lambda (_: 
+K).B) with [(Bind b0) \Rightarrow b0 | (Flat _) \Rightarrow b])])) (THead 
+(Bind b) u0 t0) (THead (Bind Abst) u t) H6) in ((let H8 \def (f_equal T T 
+(\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _) 
+\Rightarrow u0 | (TLRef _) \Rightarrow u0 | (THead _ t1 _) \Rightarrow t1])) 
+(THead (Bind b) u0 t0) (THead (Bind Abst) u t) H6) in ((let H9 \def (f_equal 
+T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _) 
+\Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ _ t1) \Rightarrow t1])) 
+(THead (Bind b) u0 t0) (THead (Bind Abst) u t) H6) in (\lambda (H10: (eq T u0 
+u)).(\lambda (H11: (eq B b Abst)).(let H12 \def (eq_ind T t0 (\lambda (t1: 
+T).((eq T t1 (THead (Bind Abst) u t)) \to (ex3_2 A A (\lambda (a3: 
+A).(\lambda (a4: A).(eq A a2 (AHead a3 a4)))) (\lambda (a3: A).(\lambda (_: 
+A).(arity g (CHead c0 (Bind b) u0) u (asucc g a3)))) (\lambda (_: A).(\lambda 
+(a4: A).(arity g (CHead (CHead c0 (Bind b) u0) (Bind Abst) u) t a4)))))) H5 t 
+H9) in (let H13 \def (eq_ind T t0 (\lambda (t1: T).(arity g (CHead c0 (Bind 
+b) u0) t1 a2)) H4 t H9) in (let H14 \def (eq_ind T u0 (\lambda (t1: T).((eq T 
+t (THead (Bind Abst) u t)) \to (ex3_2 A A (\lambda (a3: A).(\lambda (a4: 
+A).(eq A a2 (AHead a3 a4)))) (\lambda (a3: A).(\lambda (_: A).(arity g (CHead 
+c0 (Bind b) t1) u (asucc g a3)))) (\lambda (_: A).(\lambda (a4: A).(arity g 
+(CHead (CHead c0 (Bind b) t1) (Bind Abst) u) t a4)))))) H12 u H10) in (let 
+H15 \def (eq_ind T u0 (\lambda (t1: T).(arity g (CHead c0 (Bind b) t1) t a2)) 
+H13 u H10) in (let H16 \def (eq_ind T u0 (\lambda (t1: T).((eq T t1 (THead 
+(Bind Abst) u t)) \to (ex3_2 A A (\lambda (a3: A).(\lambda (a4: A).(eq A a1 
+(AHead a3 a4)))) (\lambda (a3: A).(\lambda (_: A).(arity g c0 u (asucc g 
+a3)))) (\lambda (_: A).(\lambda (a4: A).(arity g (CHead c0 (Bind Abst) u) t 
+a4)))))) H3 u H10) in (let H17 \def (eq_ind T u0 (\lambda (t1: T).(arity g c0 
+t1 a1)) H2 u H10) in (let H18 \def (eq_ind B b (\lambda (b0: B).((eq T t 
 (THead (Bind Abst) u t)) \to (ex3_2 A A (\lambda (a3: A).(\lambda (a4: A).(eq 
 A a2 (AHead a3 a4)))) (\lambda (a3: A).(\lambda (_: A).(arity g (CHead c0 
-(Bind b) u0) u (asucc g a3)))) (\lambda (_: A).(\lambda (a4: A).(arity g 
-(CHead (CHead c0 (Bind b) u0) (Bind Abst) u) t a4)))))) H5 t H9) in (let H13 
-\def (eq_ind T t0 (\lambda (t1: T).(arity g (CHead c0 (Bind b) u0) t1 a2)) H4 
-t H9) in (let H14 \def (eq_ind T u0 (\lambda (t1: T).((eq T t (THead (Bind 
+(Bind b0) u) u (asucc g a3)))) (\lambda (_: A).(\lambda (a4: A).(arity g 
+(CHead (CHead c0 (Bind b0) u) (Bind Abst) u) t a4)))))) H14 Abst H11) in (let 
+H19 \def (eq_ind B b (\lambda (b0: B).(arity g (CHead c0 (Bind b0) u) t a2)) 
+H15 Abst H11) in (let H20 \def (eq_ind B b (\lambda (b0: B).(not (eq B b0 
+Abst))) H1 Abst H11) in (let H21 \def (match (H20 (refl_equal B Abst)) in 
+False return (\lambda (_: False).(ex3_2 A A (\lambda (a3: A).(\lambda (a4: 
+A).(eq A a2 (AHead a3 a4)))) (\lambda (a3: A).(\lambda (_: A).(arity g c0 u 
+(asucc g a3)))) (\lambda (_: A).(\lambda (a4: A).(arity g (CHead c0 (Bind 
+Abst) u) t a4))))) with []) in H21))))))))))))) H8)) H7)))))))))))))) 
+(\lambda (c0: C).(\lambda (u0: T).(\lambda (a1: A).(\lambda (H1: (arity g c0 
+u0 (asucc g a1))).(\lambda (H2: (((eq T u0 (THead (Bind Abst) u t)) \to 
+(ex3_2 A A (\lambda (a2: A).(\lambda (a3: A).(eq A (asucc g a1) (AHead a2 
+a3)))) (\lambda (a2: A).(\lambda (_: A).(arity g c0 u (asucc g a2)))) 
+(\lambda (_: A).(\lambda (a3: A).(arity g (CHead c0 (Bind Abst) u) t 
+a3))))))).(\lambda (t0: T).(\lambda (a2: A).(\lambda (H3: (arity g (CHead c0 
+(Bind Abst) u0) t0 a2)).(\lambda (H4: (((eq T t0 (THead (Bind Abst) u t)) \to 
+(ex3_2 A A (\lambda (a3: A).(\lambda (a4: A).(eq A a2 (AHead a3 a4)))) 
+(\lambda (a3: A).(\lambda (_: A).(arity g (CHead c0 (Bind Abst) u0) u (asucc 
+g a3)))) (\lambda (_: A).(\lambda (a4: A).(arity g (CHead (CHead c0 (Bind 
+Abst) u0) (Bind Abst) u) t a4))))))).(\lambda (H5: (eq T (THead (Bind Abst) 
+u0 t0) (THead (Bind Abst) u t))).(let H6 \def (f_equal T T (\lambda (e: 
+T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow u0 | 
+(TLRef _) \Rightarrow u0 | (THead _ t1 _) \Rightarrow t1])) (THead (Bind 
+Abst) u0 t0) (THead (Bind Abst) u t) H5) in ((let H7 \def (f_equal T T 
+(\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _) 
+\Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ _ t1) \Rightarrow t1])) 
+(THead (Bind Abst) u0 t0) (THead (Bind Abst) u t) H5) in (\lambda (H8: (eq T 
+u0 u)).(let H9 \def (eq_ind T t0 (\lambda (t1: T).((eq T t1 (THead (Bind 
 Abst) u t)) \to (ex3_2 A A (\lambda (a3: A).(\lambda (a4: A).(eq A a2 (AHead 
-a3 a4)))) (\lambda (a3: A).(\lambda (_: A).(arity g (CHead c0 (Bind b) t1) u 
-(asucc g a3)))) (\lambda (_: A).(\lambda (a4: A).(arity g (CHead (CHead c0 
-(Bind b) t1) (Bind Abst) u) t a4)))))) H12 u H10) in (let H15 \def (eq_ind T 
-u0 (\lambda (t1: T).(arity g (CHead c0 (Bind b) t1) t a2)) H13 u H10) in (let 
-H16 \def (eq_ind T u0 (\lambda (t1: T).((eq T t1 (THead (Bind Abst) u t)) \to 
-(ex3_2 A A (\lambda (a3: A).(\lambda (a4: A).(eq A a1 (AHead a3 a4)))) 
-(\lambda (a3: A).(\lambda (_: A).(arity g c0 u (asucc g a3)))) (\lambda (_: 
-A).(\lambda (a4: A).(arity g (CHead c0 (Bind Abst) u) t a4)))))) H3 u H10) in 
-(let H17 \def (eq_ind T u0 (\lambda (t1: T).(arity g c0 t1 a1)) H2 u H10) in 
-(let H18 \def (eq_ind B b (\lambda (b0: B).((eq T t (THead (Bind Abst) u t)) 
+a3 a4)))) (\lambda (a3: A).(\lambda (_: A).(arity g (CHead c0 (Bind Abst) u0) 
+u (asucc g a3)))) (\lambda (_: A).(\lambda (a4: A).(arity g (CHead (CHead c0 
+(Bind Abst) u0) (Bind Abst) u) t a4)))))) H4 t H7) in (let H10 \def (eq_ind T 
+t0 (\lambda (t1: T).(arity g (CHead c0 (Bind Abst) u0) t1 a2)) H3 t H7) in 
+(let H11 \def (eq_ind T u0 (\lambda (t1: T).((eq T t (THead (Bind Abst) u t)) 
 \to (ex3_2 A A (\lambda (a3: A).(\lambda (a4: A).(eq A a2 (AHead a3 a4)))) 
-(\lambda (a3: A).(\lambda (_: A).(arity g (CHead c0 (Bind b0) u) u (asucc g 
-a3)))) (\lambda (_: A).(\lambda (a4: A).(arity g (CHead (CHead c0 (Bind b0) 
-u) (Bind Abst) u) t a4)))))) H14 Abst H11) in (let H19 \def (eq_ind B b 
-(\lambda (b0: B).(arity g (CHead c0 (Bind b0) u) t a2)) H15 Abst H11) in (let 
-H20 \def (eq_ind B b (\lambda (b0: B).(not (eq B b0 Abst))) H1 Abst H11) in 
-(let H21 \def (match (H20 (refl_equal B Abst)) in False return (\lambda (_: 
-False).(ex3_2 A A (\lambda (a3: A).(\lambda (a4: A).(eq A a2 (AHead a3 a4)))) 
-(\lambda (a3: A).(\lambda (_: A).(arity g c0 u (asucc g a3)))) (\lambda (_: 
-A).(\lambda (a4: A).(arity g (CHead c0 (Bind Abst) u) t a4))))) with []) in 
-H21))))))))))))) H8)) H7)))))))))))))) (\lambda (c0: C).(\lambda (u0: 
-T).(\lambda (a1: A).(\lambda (H1: (arity g c0 u0 (asucc g a1))).(\lambda (H2: 
-(((eq T u0 (THead (Bind Abst) u t)) \to (ex3_2 A A (\lambda (a2: A).(\lambda 
-(a3: A).(eq A (asucc g a1) (AHead a2 a3)))) (\lambda (a2: A).(\lambda (_: 
-A).(arity g c0 u (asucc g a2)))) (\lambda (_: A).(\lambda (a3: A).(arity g 
-(CHead c0 (Bind Abst) u) t a3))))))).(\lambda (t0: T).(\lambda (a2: 
-A).(\lambda (H3: (arity g (CHead c0 (Bind Abst) u0) t0 a2)).(\lambda (H4: 
-(((eq T t0 (THead (Bind Abst) u t)) \to (ex3_2 A A (\lambda (a3: A).(\lambda 
-(a4: A).(eq A a2 (AHead a3 a4)))) (\lambda (a3: A).(\lambda (_: A).(arity g 
-(CHead c0 (Bind Abst) u0) u (asucc g a3)))) (\lambda (_: A).(\lambda (a4: 
-A).(arity g (CHead (CHead c0 (Bind Abst) u0) (Bind Abst) u) t 
-a4))))))).(\lambda (H5: (eq T (THead (Bind Abst) u0 t0) (THead (Bind Abst) u 
-t))).(let H6 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda 
-(_: T).T) with [(TSort _) \Rightarrow u0 | (TLRef _) \Rightarrow u0 | (THead 
-_ t1 _) \Rightarrow t1])) (THead (Bind Abst) u0 t0) (THead (Bind Abst) u t) 
-H5) in ((let H7 \def (f_equal T T (\lambda (e: T).(match e in T return 
-(\lambda (_: T).T) with [(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 
-| (THead _ _ t1) \Rightarrow t1])) (THead (Bind Abst) u0 t0) (THead (Bind 
-Abst) u t) H5) in (\lambda (H8: (eq T u0 u)).(let H9 \def (eq_ind T t0 
-(\lambda (t1: T).((eq T t1 (THead (Bind Abst) u t)) \to (ex3_2 A A (\lambda 
-(a3: A).(\lambda (a4: A).(eq A a2 (AHead a3 a4)))) (\lambda (a3: A).(\lambda 
-(_: A).(arity g (CHead c0 (Bind Abst) u0) u (asucc g a3)))) (\lambda (_: 
-A).(\lambda (a4: A).(arity g (CHead (CHead c0 (Bind Abst) u0) (Bind Abst) u) 
-t a4)))))) H4 t H7) in (let H10 \def (eq_ind T t0 (\lambda (t1: T).(arity g 
-(CHead c0 (Bind Abst) u0) t1 a2)) H3 t H7) in (let H11 \def (eq_ind T u0 
-(\lambda (t1: T).((eq T t (THead (Bind Abst) u t)) \to (ex3_2 A A (\lambda 
-(a3: A).(\lambda (a4: A).(eq A a2 (AHead a3 a4)))) (\lambda (a3: A).(\lambda 
-(_: A).(arity g (CHead c0 (Bind Abst) t1) u (asucc g a3)))) (\lambda (_: 
-A).(\lambda (a4: A).(arity g (CHead (CHead c0 (Bind Abst) t1) (Bind Abst) u) 
-t a4)))))) H9 u H8) in (let H12 \def (eq_ind T u0 (\lambda (t1: T).(arity g 
-(CHead c0 (Bind Abst) t1) t a2)) H10 u H8) in (let H13 \def (eq_ind T u0 
-(\lambda (t1: T).((eq T t1 (THead (Bind Abst) u t)) \to (ex3_2 A A (\lambda 
-(a3: A).(\lambda (a4: A).(eq A (asucc g a1) (AHead a3 a4)))) (\lambda (a3: 
-A).(\lambda (_: A).(arity g c0 u (asucc g a3)))) (\lambda (_: A).(\lambda 
-(a4: A).(arity g (CHead c0 (Bind Abst) u) t a4)))))) H2 u H8) in (let H14 
-\def (eq_ind T u0 (\lambda (t1: T).(arity g c0 t1 (asucc g a1))) H1 u H8) in 
-(ex3_2_intro A A (\lambda (a3: A).(\lambda (a4: A).(eq A (AHead a1 a2) (AHead 
-a3 a4)))) (\lambda (a3: A).(\lambda (_: A).(arity g c0 u (asucc g a3)))) 
-(\lambda (_: A).(\lambda (a4: A).(arity g (CHead c0 (Bind Abst) u) t a4))) a1 
-a2 (refl_equal A (AHead a1 a2)) H14 H12))))))))) H6)))))))))))) (\lambda (c0: 
-C).(\lambda (u0: T).(\lambda (a1: A).(\lambda (_: (arity g c0 u0 
-a1)).(\lambda (_: (((eq T u0 (THead (Bind Abst) u t)) \to (ex3_2 A A (\lambda 
-(a2: A).(\lambda (a3: A).(eq A a1 (AHead a2 a3)))) (\lambda (a2: A).(\lambda 
-(_: A).(arity g c0 u (asucc g a2)))) (\lambda (_: A).(\lambda (a3: A).(arity 
-g (CHead c0 (Bind Abst) u) t a3))))))).(\lambda (t0: T).(\lambda (a2: 
-A).(\lambda (_: (arity g c0 t0 (AHead a1 a2))).(\lambda (_: (((eq T t0 (THead 
-(Bind Abst) u t)) \to (ex3_2 A A (\lambda (a3: A).(\lambda (a4: A).(eq A 
+(\lambda (a3: A).(\lambda (_: A).(arity g (CHead c0 (Bind Abst) t1) u (asucc 
+g a3)))) (\lambda (_: A).(\lambda (a4: A).(arity g (CHead (CHead c0 (Bind 
+Abst) t1) (Bind Abst) u) t a4)))))) H9 u H8) in (let H12 \def (eq_ind T u0 
+(\lambda (t1: T).(arity g (CHead c0 (Bind Abst) t1) t a2)) H10 u H8) in (let 
+H13 \def (eq_ind T u0 (\lambda (t1: T).((eq T t1 (THead (Bind Abst) u t)) \to 
+(ex3_2 A A (\lambda (a3: A).(\lambda (a4: A).(eq A (asucc g a1) (AHead a3 
+a4)))) (\lambda (a3: A).(\lambda (_: A).(arity g c0 u (asucc g a3)))) 
+(\lambda (_: A).(\lambda (a4: A).(arity g (CHead c0 (Bind Abst) u) t a4)))))) 
+H2 u H8) in (let H14 \def (eq_ind T u0 (\lambda (t1: T).(arity g c0 t1 (asucc 
+g a1))) H1 u H8) in (ex3_2_intro A A (\lambda (a3: A).(\lambda (a4: A).(eq A 
 (AHead a1 a2) (AHead a3 a4)))) (\lambda (a3: A).(\lambda (_: A).(arity g c0 u 
 (asucc g a3)))) (\lambda (_: A).(\lambda (a4: A).(arity g (CHead c0 (Bind 
-Abst) u) t a4))))))).(\lambda (H5: (eq T (THead (Flat Appl) u0 t0) (THead 
-(Bind Abst) u t))).(let H6 \def (eq_ind T (THead (Flat Appl) u0 t0) (\lambda 
-(ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) 
-\Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow 
-(match k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | 
-(Flat _) \Rightarrow True])])) I (THead (Bind Abst) u t) H5) in (False_ind 
-(ex3_2 A A (\lambda (a3: A).(\lambda (a4: A).(eq A a2 (AHead a3 a4)))) 
-(\lambda (a3: A).(\lambda (_: A).(arity g c0 u (asucc g a3)))) (\lambda (_: 
-A).(\lambda (a4: A).(arity g (CHead c0 (Bind Abst) u) t a4)))) H6)))))))))))) 
-(\lambda (c0: C).(\lambda (u0: T).(\lambda (a0: A).(\lambda (_: (arity g c0 
-u0 (asucc g a0))).(\lambda (_: (((eq T u0 (THead (Bind Abst) u t)) \to (ex3_2 
-A A (\lambda (a1: A).(\lambda (a2: A).(eq A (asucc g a0) (AHead a1 a2)))) 
-(\lambda (a1: A).(\lambda (_: A).(arity g c0 u (asucc g a1)))) (\lambda (_: 
-A).(\lambda (a2: A).(arity g (CHead c0 (Bind Abst) u) t a2))))))).(\lambda 
-(t0: T).(\lambda (_: (arity g c0 t0 a0)).(\lambda (_: (((eq T t0 (THead (Bind 
-Abst) u t)) \to (ex3_2 A A (\lambda (a1: A).(\lambda (a2: A).(eq A a0 (AHead 
-a1 a2)))) (\lambda (a1: A).(\lambda (_: A).(arity g c0 u (asucc g a1)))) 
-(\lambda (_: A).(\lambda (a2: A).(arity g (CHead c0 (Bind Abst) u) t 
-a2))))))).(\lambda (H5: (eq T (THead (Flat Cast) u0 t0) (THead (Bind Abst) u 
-t))).(let H6 \def (eq_ind T (THead (Flat Cast) u0 t0) (\lambda (ee: T).(match 
-ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | 
-(TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return 
-(\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow 
-True])])) I (THead (Bind Abst) u t) H5) in (False_ind (ex3_2 A A (\lambda 
-(a1: A).(\lambda (a2: A).(eq A a0 (AHead a1 a2)))) (\lambda (a1: A).(\lambda 
-(_: A).(arity g c0 u (asucc g a1)))) (\lambda (_: A).(\lambda (a2: A).(arity 
-g (CHead c0 (Bind Abst) u) t a2)))) H6))))))))))) (\lambda (c0: C).(\lambda 
-(t0: T).(\lambda (a1: A).(\lambda (H1: (arity g c0 t0 a1)).(\lambda (H2: 
-(((eq T t0 (THead (Bind Abst) u t)) \to (ex3_2 A A (\lambda (a2: A).(\lambda 
-(a3: A).(eq A a1 (AHead a2 a3)))) (\lambda (a2: A).(\lambda (_: A).(arity g 
-c0 u (asucc g a2)))) (\lambda (_: A).(\lambda (a3: A).(arity g (CHead c0 
-(Bind Abst) u) t a3))))))).(\lambda (a2: A).(\lambda (H3: (leq g a1 
-a2)).(\lambda (H4: (eq T t0 (THead (Bind Abst) u t))).(let H5 \def (f_equal T 
-T (\lambda (e: T).e) t0 (THead (Bind Abst) u t) H4) in (let H6 \def (eq_ind T 
-t0 (\lambda (t1: T).((eq T t1 (THead (Bind Abst) u t)) \to (ex3_2 A A 
-(\lambda (a3: A).(\lambda (a4: A).(eq A a1 (AHead a3 a4)))) (\lambda (a3: 
+Abst) u) t a4))) a1 a2 (refl_equal A (AHead a1 a2)) H14 H12))))))))) 
+H6)))))))))))) (\lambda (c0: C).(\lambda (u0: T).(\lambda (a1: A).(\lambda 
+(_: (arity g c0 u0 a1)).(\lambda (_: (((eq T u0 (THead (Bind Abst) u t)) \to 
+(ex3_2 A A (\lambda (a2: A).(\lambda (a3: A).(eq A a1 (AHead a2 a3)))) 
+(\lambda (a2: A).(\lambda (_: A).(arity g c0 u (asucc g a2)))) (\lambda (_: 
+A).(\lambda (a3: A).(arity g (CHead c0 (Bind Abst) u) t a3))))))).(\lambda 
+(t0: T).(\lambda (a2: A).(\lambda (_: (arity g c0 t0 (AHead a1 a2))).(\lambda 
+(_: (((eq T t0 (THead (Bind Abst) u t)) \to (ex3_2 A A (\lambda (a3: 
+A).(\lambda (a4: A).(eq A (AHead a1 a2) (AHead a3 a4)))) (\lambda (a3: 
 A).(\lambda (_: A).(arity g c0 u (asucc g a3)))) (\lambda (_: A).(\lambda 
-(a4: A).(arity g (CHead c0 (Bind Abst) u) t a4)))))) H2 (THead (Bind Abst) u 
-t) H5) in (let H7 \def (eq_ind T t0 (\lambda (t1: T).(arity g c0 t1 a1)) H1 
-(THead (Bind Abst) u t) H5) in (let H8 \def (H6 (refl_equal T (THead (Bind 
-Abst) u t))) in (ex3_2_ind A A (\lambda (a3: A).(\lambda (a4: A).(eq A a1 
-(AHead a3 a4)))) (\lambda (a3: A).(\lambda (_: A).(arity g c0 u (asucc g 
+(a4: A).(arity g (CHead c0 (Bind Abst) u) t a4))))))).(\lambda (H5: (eq T 
+(THead (Flat Appl) u0 t0) (THead (Bind Abst) u t))).(let H6 \def (eq_ind T 
+(THead (Flat Appl) u0 t0) (\lambda (ee: T).(match ee in T return (\lambda (_: 
+T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | 
+(THead k _ _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with 
+[(Bind _) \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind 
+Abst) u t) H5) in (False_ind (ex3_2 A A (\lambda (a3: A).(\lambda (a4: A).(eq 
+A a2 (AHead a3 a4)))) (\lambda (a3: A).(\lambda (_: A).(arity g c0 u (asucc g 
 a3)))) (\lambda (_: A).(\lambda (a4: A).(arity g (CHead c0 (Bind Abst) u) t 
-a4))) (ex3_2 A A (\lambda (a3: A).(\lambda (a4: A).(eq A a2 (AHead a3 a4)))) 
+a4)))) H6)))))))))))) (\lambda (c0: C).(\lambda (u0: T).(\lambda (a0: 
+A).(\lambda (_: (arity g c0 u0 (asucc g a0))).(\lambda (_: (((eq T u0 (THead 
+(Bind Abst) u t)) \to (ex3_2 A A (\lambda (a1: A).(\lambda (a2: A).(eq A 
+(asucc g a0) (AHead a1 a2)))) (\lambda (a1: A).(\lambda (_: A).(arity g c0 u 
+(asucc g a1)))) (\lambda (_: A).(\lambda (a2: A).(arity g (CHead c0 (Bind 
+Abst) u) t a2))))))).(\lambda (t0: T).(\lambda (_: (arity g c0 t0 
+a0)).(\lambda (_: (((eq T t0 (THead (Bind Abst) u t)) \to (ex3_2 A A (\lambda 
+(a1: A).(\lambda (a2: A).(eq A a0 (AHead a1 a2)))) (\lambda (a1: A).(\lambda 
+(_: A).(arity g c0 u (asucc g a1)))) (\lambda (_: A).(\lambda (a2: A).(arity 
+g (CHead c0 (Bind Abst) u) t a2))))))).(\lambda (H5: (eq T (THead (Flat Cast) 
+u0 t0) (THead (Bind Abst) u t))).(let H6 \def (eq_ind T (THead (Flat Cast) u0 
+t0) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort 
+_) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) 
+\Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind _) 
+\Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind Abst) u t) 
+H5) in (False_ind (ex3_2 A A (\lambda (a1: A).(\lambda (a2: A).(eq A a0 
+(AHead a1 a2)))) (\lambda (a1: A).(\lambda (_: A).(arity g c0 u (asucc g 
+a1)))) (\lambda (_: A).(\lambda (a2: A).(arity g (CHead c0 (Bind Abst) u) t 
+a2)))) H6))))))))))) (\lambda (c0: C).(\lambda (t0: T).(\lambda (a1: 
+A).(\lambda (H1: (arity g c0 t0 a1)).(\lambda (H2: (((eq T t0 (THead (Bind 
+Abst) u t)) \to (ex3_2 A A (\lambda (a2: A).(\lambda (a3: A).(eq A a1 (AHead 
+a2 a3)))) (\lambda (a2: A).(\lambda (_: A).(arity g c0 u (asucc g a2)))) 
+(\lambda (_: A).(\lambda (a3: A).(arity g (CHead c0 (Bind Abst) u) t 
+a3))))))).(\lambda (a2: A).(\lambda (H3: (leq g a1 a2)).(\lambda (H4: (eq T 
+t0 (THead (Bind Abst) u t))).(let H5 \def (f_equal T T (\lambda (e: T).e) t0 
+(THead (Bind Abst) u t) H4) in (let H6 \def (eq_ind T t0 (\lambda (t1: 
+T).((eq T t1 (THead (Bind Abst) u t)) \to (ex3_2 A A (\lambda (a3: 
+A).(\lambda (a4: A).(eq A a1 (AHead a3 a4)))) (\lambda (a3: A).(\lambda (_: 
+A).(arity g c0 u (asucc g a3)))) (\lambda (_: A).(\lambda (a4: A).(arity g 
+(CHead c0 (Bind Abst) u) t a4)))))) H2 (THead (Bind Abst) u t) H5) in (let H7 
+\def (eq_ind T t0 (\lambda (t1: T).(arity g c0 t1 a1)) H1 (THead (Bind Abst) 
+u t) H5) in (let H8 \def (H6 (refl_equal T (THead (Bind Abst) u t))) in 
+(ex3_2_ind A A (\lambda (a3: A).(\lambda (a4: A).(eq A a1 (AHead a3 a4)))) 
 (\lambda (a3: A).(\lambda (_: A).(arity g c0 u (asucc g a3)))) (\lambda (_: 
-A).(\lambda (a4: A).(arity g (CHead c0 (Bind Abst) u) t a4)))) (\lambda (x0: 
-A).(\lambda (x1: A).(\lambda (H9: (eq A a1 (AHead x0 x1))).(\lambda (H10: 
-(arity g c0 u (asucc g x0))).(\lambda (H11: (arity g (CHead c0 (Bind Abst) u) 
-t x1)).(let H12 \def (eq_ind A a1 (\lambda (a0: A).(leq g a0 a2)) H3 (AHead 
-x0 x1) H9) in (let H13 \def (eq_ind A a1 (\lambda (a0: A).(arity g c0 (THead 
-(Bind Abst) u t) a0)) H7 (AHead x0 x1) H9) in (let H_x \def (leq_gen_head g 
-x0 x1 a2 H12) in (let H14 \def H_x in (ex3_2_ind A A (\lambda (a3: 
+A).(\lambda (a4: A).(arity g (CHead c0 (Bind Abst) u) t a4))) (ex3_2 A A 
+(\lambda (a3: A).(\lambda (a4: A).(eq A a2 (AHead a3 a4)))) (\lambda (a3: 
+A).(\lambda (_: A).(arity g c0 u (asucc g a3)))) (\lambda (_: A).(\lambda 
+(a4: A).(arity g (CHead c0 (Bind Abst) u) t a4)))) (\lambda (x0: A).(\lambda 
+(x1: A).(\lambda (H9: (eq A a1 (AHead x0 x1))).(\lambda (H10: (arity g c0 u 
+(asucc g x0))).(\lambda (H11: (arity g (CHead c0 (Bind Abst) u) t x1)).(let 
+H12 \def (eq_ind A a1 (\lambda (a0: A).(leq g a0 a2)) H3 (AHead x0 x1) H9) in 
+(let H13 \def (eq_ind A a1 (\lambda (a0: A).(arity g c0 (THead (Bind Abst) u 
+t) a0)) H7 (AHead x0 x1) H9) in (let H_x \def (leq_gen_head g x0 x1 a2 H12) 
+in (let H14 \def H_x in (ex3_2_ind A A (\lambda (a3: A).(\lambda (a4: A).(eq 
+A a2 (AHead a3 a4)))) (\lambda (a3: A).(\lambda (_: A).(leq g x0 a3))) 
+(\lambda (_: A).(\lambda (a4: A).(leq g x1 a4))) (ex3_2 A A (\lambda (a3: 
 A).(\lambda (a4: A).(eq A a2 (AHead a3 a4)))) (\lambda (a3: A).(\lambda (_: 
-A).(leq g x0 a3))) (\lambda (_: A).(\lambda (a4: A).(leq g x1 a4))) (ex3_2 A 
-A (\lambda (a3: A).(\lambda (a4: A).(eq A a2 (AHead a3 a4)))) (\lambda (a3: 
+A).(arity g c0 u (asucc g a3)))) (\lambda (_: A).(\lambda (a4: A).(arity g 
+(CHead c0 (Bind Abst) u) t a4)))) (\lambda (x2: A).(\lambda (x3: A).(\lambda 
+(H15: (eq A a2 (AHead x2 x3))).(\lambda (H16: (leq g x0 x2)).(\lambda (H17: 
+(leq g x1 x3)).(eq_ind_r A (AHead x2 x3) (\lambda (a0: A).(ex3_2 A A (\lambda 
+(a3: A).(\lambda (a4: A).(eq A a0 (AHead a3 a4)))) (\lambda (a3: A).(\lambda 
+(_: A).(arity g c0 u (asucc g a3)))) (\lambda (_: A).(\lambda (a4: A).(arity 
+g (CHead c0 (Bind Abst) u) t a4))))) (ex3_2_intro A A (\lambda (a3: 
+A).(\lambda (a4: A).(eq A (AHead x2 x3) (AHead a3 a4)))) (\lambda (a3: 
 A).(\lambda (_: A).(arity g c0 u (asucc g a3)))) (\lambda (_: A).(\lambda 
-(a4: A).(arity g (CHead c0 (Bind Abst) u) t a4)))) (\lambda (x2: A).(\lambda 
-(x3: A).(\lambda (H15: (eq A a2 (AHead x2 x3))).(\lambda (H16: (leq g x0 
-x2)).(\lambda (H17: (leq g x1 x3)).(eq_ind_r A (AHead x2 x3) (\lambda (a0: 
-A).(ex3_2 A A (\lambda (a3: A).(\lambda (a4: A).(eq A a0 (AHead a3 a4)))) 
-(\lambda (a3: A).(\lambda (_: A).(arity g c0 u (asucc g a3)))) (\lambda (_: 
-A).(\lambda (a4: A).(arity g (CHead c0 (Bind Abst) u) t a4))))) (ex3_2_intro 
-A A (\lambda (a3: A).(\lambda (a4: A).(eq A (AHead x2 x3) (AHead a3 a4)))) 
-(\lambda (a3: A).(\lambda (_: A).(arity g c0 u (asucc g a3)))) (\lambda (_: 
-A).(\lambda (a4: A).(arity g (CHead c0 (Bind Abst) u) t a4))) x2 x3 
-(refl_equal A (AHead x2 x3)) (arity_repl g c0 u (asucc g x0) H10 (asucc g x2) 
-(asucc_repl g x0 x2 H16)) (arity_repl g (CHead c0 (Bind Abst) u) t x1 H11 x3 
-H17)) a2 H15)))))) H14)))))))))) H8))))))))))))) c y a H0))) H)))))).
+(a4: A).(arity g (CHead c0 (Bind Abst) u) t a4))) x2 x3 (refl_equal A (AHead 
+x2 x3)) (arity_repl g c0 u (asucc g x0) H10 (asucc g x2) (asucc_repl g x0 x2 
+H16)) (arity_repl g (CHead c0 (Bind Abst) u) t x1 H11 x3 H17)) a2 H15)))))) 
+H14)))))))))) H8))))))))))))) c y a H0))) H)))))).
 
 theorem arity_gen_appl:
  \forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t: T).(\forall (a2: 
@@ -689,27 +691,27 @@ g c u a1)) (\lambda (a1: A).(arity g c t (AHead a1 a2)))))))))
 \def
  \lambda (g: G).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(\lambda (a2: 
 A).(\lambda (H: (arity g c (THead (Flat Appl) u t) a2)).(insert_eq T (THead 
-(Flat Appl) u t) (\lambda (t0: T).(arity g c t0 a2)) (ex2 A (\lambda (a1: 
-A).(arity g c u a1)) (\lambda (a1: A).(arity g c t (AHead a1 a2)))) (\lambda 
-(y: T).(\lambda (H0: (arity g c y a2)).(arity_ind g (\lambda (c0: C).(\lambda 
-(t0: T).(\lambda (a: A).((eq T t0 (THead (Flat Appl) u t)) \to (ex2 A 
-(\lambda (a1: A).(arity g c0 u a1)) (\lambda (a1: A).(arity g c0 t (AHead a1 
-a)))))))) (\lambda (c0: C).(\lambda (n: nat).(\lambda (H1: (eq T (TSort n) 
-(THead (Flat Appl) u t))).(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 
-(THead (Flat Appl) u t) H1) in (False_ind (ex2 A (\lambda (a1: A).(arity g c0 
-u a1)) (\lambda (a1: A).(arity g c0 t (AHead a1 (ASort O n))))) H2))))) 
-(\lambda (c0: C).(\lambda (d: C).(\lambda (u0: T).(\lambda (i: nat).(\lambda 
-(_: (getl i c0 (CHead d (Bind Abbr) u0))).(\lambda (a: A).(\lambda (_: (arity 
-g d u0 a)).(\lambda (_: (((eq T u0 (THead (Flat Appl) u t)) \to (ex2 A 
-(\lambda (a1: A).(arity g d u a1)) (\lambda (a1: A).(arity g d t (AHead a1 
-a))))))).(\lambda (H4: (eq T (TLRef i) (THead (Flat Appl) u t))).(let H5 \def 
-(eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T return (\lambda (_: 
-T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | 
-(THead _ _ _) \Rightarrow False])) I (THead (Flat Appl) u t) H4) in 
-(False_ind (ex2 A (\lambda (a1: A).(arity g c0 u a1)) (\lambda (a1: A).(arity 
-g c0 t (AHead a1 a)))) H5))))))))))) (\lambda (c0: C).(\lambda (d: 
+(Flat Appl) u t) (\lambda (t0: T).(arity g c t0 a2)) (\lambda (_: T).(ex2 A 
+(\lambda (a1: A).(arity g c u a1)) (\lambda (a1: A).(arity g c t (AHead a1 
+a2))))) (\lambda (y: T).(\lambda (H0: (arity g c y a2)).(arity_ind g (\lambda 
+(c0: C).(\lambda (t0: T).(\lambda (a: A).((eq T t0 (THead (Flat Appl) u t)) 
+\to (ex2 A (\lambda (a1: A).(arity g c0 u a1)) (\lambda (a1: A).(arity g c0 t 
+(AHead a1 a)))))))) (\lambda (c0: C).(\lambda (n: nat).(\lambda (H1: (eq T 
+(TSort n) (THead (Flat Appl) u t))).(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 (THead (Flat Appl) u t) H1) in (False_ind (ex2 A (\lambda (a1: 
+A).(arity g c0 u a1)) (\lambda (a1: A).(arity g c0 t (AHead a1 (ASort O 
+n))))) H2))))) (\lambda (c0: C).(\lambda (d: C).(\lambda (u0: T).(\lambda (i: 
+nat).(\lambda (_: (getl i c0 (CHead d (Bind Abbr) u0))).(\lambda (a: 
+A).(\lambda (_: (arity g d u0 a)).(\lambda (_: (((eq T u0 (THead (Flat Appl) 
+u t)) \to (ex2 A (\lambda (a1: A).(arity g d u a1)) (\lambda (a1: A).(arity g 
+d t (AHead a1 a))))))).(\lambda (H4: (eq T (TLRef i) (THead (Flat Appl) u 
+t))).(let H5 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T return 
+(\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) 
+\Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead (Flat Appl) u 
+t) H4) in (False_ind (ex2 A (\lambda (a1: A).(arity g c0 u a1)) (\lambda (a1: 
+A).(arity g c0 t (AHead a1 a)))) H5))))))))))) (\lambda (c0: C).(\lambda (d: 
 C).(\lambda (u0: T).(\lambda (i: nat).(\lambda (_: (getl i c0 (CHead d (Bind 
 Abst) u0))).(\lambda (a: A).(\lambda (_: (arity g d u0 (asucc g a))).(\lambda 
 (_: (((eq T u0 (THead (Flat Appl) u t)) \to (ex2 A (\lambda (a1: A).(arity g 
@@ -811,22 +813,22 @@ A).((arity g c (THead (Flat Cast) u t) a) \to (land (arity g c u (asucc g a))
 \def
  \lambda (g: G).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(\lambda (a: 
 A).(\lambda (H: (arity g c (THead (Flat Cast) u t) a)).(insert_eq T (THead 
-(Flat Cast) u t) (\lambda (t0: T).(arity g c t0 a)) (land (arity g c u (asucc 
-g a)) (arity g c t a)) (\lambda (y: T).(\lambda (H0: (arity g c y 
-a)).(arity_ind g (\lambda (c0: C).(\lambda (t0: T).(\lambda (a0: A).((eq T t0 
-(THead (Flat Cast) u t)) \to (land (arity g c0 u (asucc g a0)) (arity g c0 t 
-a0)))))) (\lambda (c0: C).(\lambda (n: nat).(\lambda (H1: (eq T (TSort n) 
-(THead (Flat Cast) u t))).(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 
-(THead (Flat Cast) u t) H1) in (False_ind (land (arity g c0 u (asucc g (ASort 
-O n))) (arity g c0 t (ASort O n))) H2))))) (\lambda (c0: C).(\lambda (d: 
-C).(\lambda (u0: T).(\lambda (i: nat).(\lambda (_: (getl i c0 (CHead d (Bind 
-Abbr) u0))).(\lambda (a0: A).(\lambda (_: (arity g d u0 a0)).(\lambda (_: 
-(((eq T u0 (THead (Flat Cast) u t)) \to (land (arity g d u (asucc g a0)) 
-(arity g d t a0))))).(\lambda (H4: (eq T (TLRef i) (THead (Flat Cast) u 
-t))).(let H5 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T return 
-(\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) 
+(Flat Cast) u t) (\lambda (t0: T).(arity g c t0 a)) (\lambda (_: T).(land 
+(arity g c u (asucc g a)) (arity g c t a))) (\lambda (y: T).(\lambda (H0: 
+(arity g c y a)).(arity_ind g (\lambda (c0: C).(\lambda (t0: T).(\lambda (a0: 
+A).((eq T t0 (THead (Flat Cast) u t)) \to (land (arity g c0 u (asucc g a0)) 
+(arity g c0 t a0)))))) (\lambda (c0: C).(\lambda (n: nat).(\lambda (H1: (eq T 
+(TSort n) (THead (Flat Cast) u t))).(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 (THead (Flat Cast) u t) H1) in (False_ind (land (arity g c0 u 
+(asucc g (ASort O n))) (arity g c0 t (ASort O n))) H2))))) (\lambda (c0: 
+C).(\lambda (d: C).(\lambda (u0: T).(\lambda (i: nat).(\lambda (_: (getl i c0 
+(CHead d (Bind Abbr) u0))).(\lambda (a0: A).(\lambda (_: (arity g d u0 
+a0)).(\lambda (_: (((eq T u0 (THead (Flat Cast) u t)) \to (land (arity g d u 
+(asucc g a0)) (arity g d t a0))))).(\lambda (H4: (eq T (TLRef i) (THead (Flat 
+Cast) u t))).(let H5 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T 
+return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) 
 \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead (Flat Cast) u 
 t) H4) in (False_ind (land (arity g c0 u (asucc g a0)) (arity g c0 t a0)) 
 H5))))))))))) (\lambda (c0: C).(\lambda (d: C).(\lambda (u0: T).(\lambda (i: 
@@ -943,22 +945,22 @@ C).((drop h d c1 c2) \to (arity g c2 t a)))))))))
 \def
  \lambda (g: G).(\lambda (c1: C).(\lambda (t: T).(\lambda (a: A).(\lambda (h: 
 nat).(\lambda (d: nat).(\lambda (H: (arity g c1 (lift h d t) a)).(insert_eq T 
-(lift h d t) (\lambda (t0: T).(arity g c1 t0 a)) (\forall (c2: C).((drop h d 
-c1 c2) \to (arity g c2 t a))) (\lambda (y: T).(\lambda (H0: (arity g c1 y 
-a)).(unintro T t (\lambda (t0: T).((eq T y (lift h d t0)) \to (\forall (c2: 
-C).((drop h d c1 c2) \to (arity g c2 t0 a))))) (unintro nat d (\lambda (n: 
-nat).(\forall (x: T).((eq T y (lift h n x)) \to (\forall (c2: C).((drop h n 
-c1 c2) \to (arity g c2 x a)))))) (arity_ind g (\lambda (c: C).(\lambda (t0: 
-T).(\lambda (a0: A).(\forall (x: nat).(\forall (x0: T).((eq T t0 (lift h x 
-x0)) \to (\forall (c2: C).((drop h x c c2) \to (arity g c2 x0 a0))))))))) 
-(\lambda (c: C).(\lambda (n: nat).(\lambda (x: nat).(\lambda (x0: T).(\lambda 
-(H1: (eq T (TSort n) (lift h x x0))).(\lambda (c2: C).(\lambda (_: (drop h x 
-c c2)).(eq_ind_r T (TSort n) (\lambda (t0: T).(arity g c2 t0 (ASort O n))) 
-(arity_sort g c2 n) x0 (lift_gen_sort h x n x0 H1))))))))) (\lambda (c: 
-C).(\lambda (d0: C).(\lambda (u: T).(\lambda (i: nat).(\lambda (H1: (getl i c 
-(CHead d0 (Bind Abbr) u))).(\lambda (a0: A).(\lambda (H2: (arity g d0 u 
-a0)).(\lambda (H3: ((\forall (x: nat).(\forall (x0: T).((eq T u (lift h x 
-x0)) \to (\forall (c2: C).((drop h x d0 c2) \to (arity g c2 x0 
+(lift h d t) (\lambda (t0: T).(arity g c1 t0 a)) (\lambda (_: T).(\forall 
+(c2: C).((drop h d c1 c2) \to (arity g c2 t a)))) (\lambda (y: T).(\lambda 
+(H0: (arity g c1 y a)).(unintro T t (\lambda (t0: T).((eq T y (lift h d t0)) 
+\to (\forall (c2: C).((drop h d c1 c2) \to (arity g c2 t0 a))))) (unintro nat 
+d (\lambda (n: nat).(\forall (x: T).((eq T y (lift h n x)) \to (\forall (c2: 
+C).((drop h n c1 c2) \to (arity g c2 x a)))))) (arity_ind g (\lambda (c: 
+C).(\lambda (t0: T).(\lambda (a0: A).(\forall (x: nat).(\forall (x0: T).((eq 
+T t0 (lift h x x0)) \to (\forall (c2: C).((drop h x c c2) \to (arity g c2 x0 
+a0))))))))) (\lambda (c: C).(\lambda (n: nat).(\lambda (x: nat).(\lambda (x0: 
+T).(\lambda (H1: (eq T (TSort n) (lift h x x0))).(\lambda (c2: C).(\lambda 
+(_: (drop h x c c2)).(eq_ind_r T (TSort n) (\lambda (t0: T).(arity g c2 t0 
+(ASort O n))) (arity_sort g c2 n) x0 (lift_gen_sort h x n x0 H1))))))))) 
+(\lambda (c: C).(\lambda (d0: C).(\lambda (u: T).(\lambda (i: nat).(\lambda 
+(H1: (getl i c (CHead d0 (Bind Abbr) u))).(\lambda (a0: A).(\lambda (H2: 
+(arity g d0 u a0)).(\lambda (H3: ((\forall (x: nat).(\forall (x0: T).((eq T u 
+(lift h x x0)) \to (\forall (c2: C).((drop h x d0 c2) \to (arity g c2 x0 
 a0)))))))).(\lambda (x: nat).(\lambda (x0: T).(\lambda (H4: (eq T (TLRef i) 
 (lift h x x0))).(\lambda (c2: C).(\lambda (H5: (drop h x c c2)).(let H_x \def 
 (lift_gen_lref x0 x h i H4) in (let H6 \def H_x in (or_ind (land (lt i x) (eq