(* This file was automatically generated: do not edit *********************)
-
+set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/fwd".
include "arity/defs.ma".
\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
\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))))
\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 |
\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:
\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
\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:
\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