-(fsubst0 i u c (TSort n) c2 t2)).(let H2 \def (fsubst0_gen_base c c2 (TSort
-n) t2 u i H1) in (or3_ind (land (eq C c c2) (subst0 i u (TSort n) t2)) (land
-(eq T (TSort n) t2) (csubst0 i u c c2)) (land (subst0 i u (TSort n) t2)
-(csubst0 i u c c2)) (arity g c2 t2 (ASort O n)) (\lambda (H3: (land (eq C c
-c2) (subst0 i u (TSort n) t2))).(and_ind (eq C c c2) (subst0 i u (TSort n)
-t2) (arity g c2 t2 (ASort O n)) (\lambda (H4: (eq C c c2)).(\lambda (H5:
-(subst0 i u (TSort n) t2)).(eq_ind C c (\lambda (c0: C).(arity g c0 t2 (ASort
-O n))) (subst0_gen_sort u t2 i n H5 (arity g c t2 (ASort O n))) c2 H4))) H3))
-(\lambda (H3: (land (eq T (TSort n) t2) (csubst0 i u c c2))).(and_ind (eq T
-(TSort n) t2) (csubst0 i u c c2) (arity g c2 t2 (ASort O n)) (\lambda (H4:
-(eq T (TSort n) t2)).(\lambda (_: (csubst0 i u c c2)).(eq_ind T (TSort n)
-(\lambda (t: T).(arity g c2 t (ASort O n))) (arity_sort g c2 n) t2 H4))) H3))
-(\lambda (H3: (land (subst0 i u (TSort n) t2) (csubst0 i u c c2))).(and_ind
-(subst0 i u (TSort n) t2) (csubst0 i u c c2) (arity g c2 t2 (ASort O n))
-(\lambda (H4: (subst0 i u (TSort n) t2)).(\lambda (_: (csubst0 i u c
-c2)).(subst0_gen_sort u t2 i n H4 (arity g c2 t2 (ASort O n))))) H3))
-H2))))))))))) (\lambda (c: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i:
-nat).(\lambda (H0: (getl i c (CHead d (Bind Abbr) u))).(\lambda (a0:
-A).(\lambda (H1: (arity g d u a0)).(\lambda (H2: ((\forall (d1: C).(\forall
-(u0: T).(\forall (i0: nat).((getl i0 d (CHead d1 (Bind Abbr) u0)) \to
-(\forall (c2: C).(\forall (t2: T).((fsubst0 i0 u0 d u c2 t2) \to (arity g c2
-t2 a0)))))))))).(\lambda (d1: C).(\lambda (u0: T).(\lambda (i0: nat).(\lambda
-(H3: (getl i0 c (CHead d1 (Bind Abbr) u0))).(\lambda (c2: C).(\lambda (t2:
-T).(\lambda (H4: (fsubst0 i0 u0 c (TLRef i) c2 t2)).(let H5 \def
-(fsubst0_gen_base c c2 (TLRef i) t2 u0 i0 H4) in (or3_ind (land (eq C c c2)
-(subst0 i0 u0 (TLRef i) t2)) (land (eq T (TLRef i) t2) (csubst0 i0 u0 c c2))
-(land (subst0 i0 u0 (TLRef i) t2) (csubst0 i0 u0 c c2)) (arity g c2 t2 a0)
-(\lambda (H6: (land (eq C c c2) (subst0 i0 u0 (TLRef i) t2))).(and_ind (eq C
-c c2) (subst0 i0 u0 (TLRef i) t2) (arity g c2 t2 a0) (\lambda (H7: (eq C c
-c2)).(\lambda (H8: (subst0 i0 u0 (TLRef i) t2)).(eq_ind C c (\lambda (c0:
-C).(arity g c0 t2 a0)) (and_ind (eq nat i i0) (eq T t2 (lift (S i) O u0))
-(arity g c t2 a0) (\lambda (H9: (eq nat i i0)).(\lambda (H10: (eq T t2 (lift
-(S i) O u0))).(eq_ind_r T (lift (S i) O u0) (\lambda (t: T).(arity g c t a0))
-(let H11 \def (eq_ind_r nat i0 (\lambda (n: nat).(getl n c (CHead d1 (Bind
-Abbr) u0))) H3 i H9) in (let H12 \def (eq_ind C (CHead d (Bind Abbr) u)
-(\lambda (c0: C).(getl i c c0)) H0 (CHead d1 (Bind Abbr) u0) (getl_mono c
-(CHead d (Bind Abbr) u) i H0 (CHead d1 (Bind Abbr) u0) H11)) in (let H13 \def
-(f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with
-[(CSort _) \Rightarrow d | (CHead c0 _ _) \Rightarrow c0])) (CHead d (Bind
-Abbr) u) (CHead d1 (Bind Abbr) u0) (getl_mono c (CHead d (Bind Abbr) u) i H0
-(CHead d1 (Bind Abbr) u0) H11)) in ((let H14 \def (f_equal C T (\lambda (e:
-C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u |
-(CHead _ _ t) \Rightarrow t])) (CHead d (Bind Abbr) u) (CHead d1 (Bind Abbr)
-u0) (getl_mono c (CHead d (Bind Abbr) u) i H0 (CHead d1 (Bind Abbr) u0) H11))
-in (\lambda (H15: (eq C d d1)).(let H16 \def (eq_ind_r T u0 (\lambda (t:
-T).(getl i c (CHead d1 (Bind Abbr) t))) H12 u H14) in (eq_ind T u (\lambda
-(t: T).(arity g c (lift (S i) O t) a0)) (let H17 \def (eq_ind_r C d1 (\lambda
-(c0: C).(getl i c (CHead c0 (Bind Abbr) u))) H16 d H15) in (arity_lift g d u
-a0 H1 c (S i) O (getl_drop Abbr c d u i H17))) u0 H14)))) H13)))) t2 H10)))
-(subst0_gen_lref u0 t2 i0 i H8)) c2 H7))) H6)) (\lambda (H6: (land (eq T
-(TLRef i) t2) (csubst0 i0 u0 c c2))).(and_ind (eq T (TLRef i) t2) (csubst0 i0
-u0 c c2) (arity g c2 t2 a0) (\lambda (H7: (eq T (TLRef i) t2)).(\lambda (H8:
-(csubst0 i0 u0 c c2)).(eq_ind T (TLRef i) (\lambda (t: T).(arity g c2 t a0))
-(lt_le_e i i0 (arity g c2 (TLRef i) a0) (\lambda (H9: (lt i i0)).(let H10
-\def (csubst0_getl_lt i0 i H9 c c2 u0 H8 (CHead d (Bind Abbr) u) H0) in
-(or4_ind (getl i c2 (CHead d (Bind Abbr) u)) (ex3_4 B C T T (\lambda (b:
-B).(\lambda (e0: C).(\lambda (u1: T).(\lambda (_: T).(eq C (CHead d (Bind
-Abbr) u) (CHead e0 (Bind b) u1)))))) (\lambda (b: B).(\lambda (e0:
-C).(\lambda (_: T).(\lambda (w: T).(getl i c2 (CHead e0 (Bind b) w))))))
-(\lambda (_: B).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0
-(minus i0 (S i)) u0 u1 w)))))) (ex3_4 B C C T (\lambda (b: B).(\lambda (e1:
-C).(\lambda (_: C).(\lambda (u1: T).(eq C (CHead d (Bind Abbr) u) (CHead e1
-(Bind b) u1)))))) (\lambda (b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda
-(u1: T).(getl i c2 (CHead e2 (Bind b) u1)))))) (\lambda (_: B).(\lambda (e1:
-C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (minus i0 (S i)) u0 e1 e2))))))
-(ex4_5 B C C T T (\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda
-(u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b)
-u1))))))) (\lambda (b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda (_:
-T).(\lambda (w: T).(getl i c2 (CHead e2 (Bind b) w))))))) (\lambda (_:
-B).(\lambda (_: C).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0
-(minus i0 (S i)) u0 u1 w)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2:
-C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus i0 (S i)) u0 e1 e2)))))))
-(arity g c2 (TLRef i) a0) (\lambda (H11: (getl i c2 (CHead d (Bind Abbr)
-u))).(let H12 \def (eq_ind nat (minus i0 i) (\lambda (n: nat).(getl n (CHead
-d (Bind Abbr) u) (CHead d1 (Bind Abbr) u0))) (getl_conf_le i0 (CHead d1 (Bind
-Abbr) u0) c H3 (CHead d (Bind Abbr) u) i H0 (le_S_n i i0 (le_S (S i) i0 H9)))
-(S (minus i0 (S i))) (minus_x_Sy i0 i H9)) in (arity_abbr g c2 d u i H11 a0
-H1))) (\lambda (H11: (ex3_4 B C T T (\lambda (b: B).(\lambda (e0: C).(\lambda
-(u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead e0 (Bind b)
-u1)))))) (\lambda (b: B).(\lambda (e0: C).(\lambda (_: T).(\lambda (w:
-T).(getl i c2 (CHead e0 (Bind b) w)))))) (\lambda (_: B).(\lambda (_:
-C).(\lambda (u1: T).(\lambda (w: T).(subst0 (minus i0 (S i)) u0 u1
-w))))))).(ex3_4_ind B C T T (\lambda (b: B).(\lambda (e0: C).(\lambda (u1:
-T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead e0 (Bind b) u1))))))
-(\lambda (b: B).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(getl i c2
-(CHead e0 (Bind b) w)))))) (\lambda (_: B).(\lambda (_: C).(\lambda (u1:
-T).(\lambda (w: T).(subst0 (minus i0 (S i)) u0 u1 w))))) (arity g c2 (TLRef
-i) a0) (\lambda (x0: B).(\lambda (x1: C).(\lambda (x2: T).(\lambda (x3:
-T).(\lambda (H12: (eq C (CHead d (Bind Abbr) u) (CHead x1 (Bind x0)
-x2))).(\lambda (H13: (getl i c2 (CHead x1 (Bind x0) x3))).(\lambda (H14:
-(subst0 (minus i0 (S i)) u0 x2 x3)).(let H15 \def (eq_ind nat (minus i0 i)
-(\lambda (n: nat).(getl n (CHead d (Bind Abbr) u) (CHead d1 (Bind Abbr) u0)))
-(getl_conf_le i0 (CHead d1 (Bind Abbr) u0) c H3 (CHead d (Bind Abbr) u) i H0
-(le_S_n i i0 (le_S (S i) i0 H9))) (S (minus i0 (S i))) (minus_x_Sy i0 i H9))
-in (let H16 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda
-(_: C).C) with [(CSort _) \Rightarrow d | (CHead c0 _ _) \Rightarrow c0]))
-(CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x2) H12) in ((let H17 \def
-(f_equal C B (\lambda (e: C).(match e in C return (\lambda (_: C).B) with
-[(CSort _) \Rightarrow Abbr | (CHead _ k _) \Rightarrow (match k in K return
-(\lambda (_: K).B) with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow
-Abbr])])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x2) H12) in ((let H18
-\def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T)
-with [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow t])) (CHead d (Bind
-Abbr) u) (CHead x1 (Bind x0) x2) H12) in (\lambda (H19: (eq B Abbr
-x0)).(\lambda (H20: (eq C d x1)).(let H21 \def (eq_ind_r T x2 (\lambda (t:
-T).(subst0 (minus i0 (S i)) u0 t x3)) H14 u H18) in (let H22 \def (eq_ind_r C
-x1 (\lambda (c0: C).(getl i c2 (CHead c0 (Bind x0) x3))) H13 d H20) in (let
-H23 \def (eq_ind_r B x0 (\lambda (b: B).(getl i c2 (CHead d (Bind b) x3)))
-H22 Abbr H19) in (arity_abbr g c2 d x3 i H23 a0 (H2 d1 u0 (r (Bind Abbr)
-(minus i0 (S i))) (getl_gen_S (Bind Abbr) d (CHead d1 (Bind Abbr) u0) u
-(minus i0 (S i)) H15) d x3 (fsubst0_snd (r (Bind Abbr) (minus i0 (S i))) u0 d
-u x3 H21))))))))) H17)) H16)))))))))) H11)) (\lambda (H11: (ex3_4 B C C T
-(\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(eq C
-(CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1)))))) (\lambda (b: B).(\lambda
-(_: C).(\lambda (e2: C).(\lambda (u1: T).(getl i c2 (CHead e2 (Bind b)
-u1)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
-T).(csubst0 (minus i0 (S i)) u0 e1 e2))))))).(ex3_4_ind B C C T (\lambda (b:
+(fsubst0 i u c (TSort n) c2 t2)).(let H_x \def (fsubst0_gen_base c c2 (TSort
+n) t2 u i H1) in (let H2 \def H_x in (or3_ind (land (eq C c c2) (subst0 i u
+(TSort n) t2)) (land (eq T (TSort n) t2) (csubst0 i u c c2)) (land (subst0 i
+u (TSort n) t2) (csubst0 i u c c2)) (arity g c2 t2 (ASort O n)) (\lambda (H3:
+(land (eq C c c2) (subst0 i u (TSort n) t2))).(and_ind (eq C c c2) (subst0 i
+u (TSort n) t2) (arity g c2 t2 (ASort O n)) (\lambda (H4: (eq C c
+c2)).(\lambda (H5: (subst0 i u (TSort n) t2)).(eq_ind C c (\lambda (c0:
+C).(arity g c0 t2 (ASort O n))) (subst0_gen_sort u t2 i n H5 (arity g c t2
+(ASort O n))) c2 H4))) H3)) (\lambda (H3: (land (eq T (TSort n) t2) (csubst0
+i u c c2))).(and_ind (eq T (TSort n) t2) (csubst0 i u c c2) (arity g c2 t2
+(ASort O n)) (\lambda (H4: (eq T (TSort n) t2)).(\lambda (_: (csubst0 i u c
+c2)).(eq_ind T (TSort n) (\lambda (t: T).(arity g c2 t (ASort O n)))
+(arity_sort g c2 n) t2 H4))) H3)) (\lambda (H3: (land (subst0 i u (TSort n)
+t2) (csubst0 i u c c2))).(and_ind (subst0 i u (TSort n) t2) (csubst0 i u c
+c2) (arity g c2 t2 (ASort O n)) (\lambda (H4: (subst0 i u (TSort n)
+t2)).(\lambda (_: (csubst0 i u c c2)).(subst0_gen_sort u t2 i n H4 (arity g
+c2 t2 (ASort O n))))) H3)) H2)))))))))))) (\lambda (c: C).(\lambda (d:
+C).(\lambda (u: T).(\lambda (i: nat).(\lambda (H0: (getl i c (CHead d (Bind
+Abbr) u))).(\lambda (a0: A).(\lambda (H1: (arity g d u a0)).(\lambda (H2:
+((\forall (d1: C).(\forall (u0: T).(\forall (i0: nat).((getl i0 d (CHead d1
+(Bind Abbr) u0)) \to (\forall (c2: C).(\forall (t2: T).((fsubst0 i0 u0 d u c2
+t2) \to (arity g c2 t2 a0)))))))))).(\lambda (d1: C).(\lambda (u0:
+T).(\lambda (i0: nat).(\lambda (H3: (getl i0 c (CHead d1 (Bind Abbr)
+u0))).(\lambda (c2: C).(\lambda (t2: T).(\lambda (H4: (fsubst0 i0 u0 c (TLRef
+i) c2 t2)).(let H_x \def (fsubst0_gen_base c c2 (TLRef i) t2 u0 i0 H4) in
+(let H5 \def H_x in (or3_ind (land (eq C c c2) (subst0 i0 u0 (TLRef i) t2))
+(land (eq T (TLRef i) t2) (csubst0 i0 u0 c c2)) (land (subst0 i0 u0 (TLRef i)
+t2) (csubst0 i0 u0 c c2)) (arity g c2 t2 a0) (\lambda (H6: (land (eq C c c2)
+(subst0 i0 u0 (TLRef i) t2))).(and_ind (eq C c c2) (subst0 i0 u0 (TLRef i)
+t2) (arity g c2 t2 a0) (\lambda (H7: (eq C c c2)).(\lambda (H8: (subst0 i0 u0
+(TLRef i) t2)).(eq_ind C c (\lambda (c0: C).(arity g c0 t2 a0)) (and_ind (eq
+nat i i0) (eq T t2 (lift (S i) O u0)) (arity g c t2 a0) (\lambda (H9: (eq nat
+i i0)).(\lambda (H10: (eq T t2 (lift (S i) O u0))).(eq_ind_r T (lift (S i) O
+u0) (\lambda (t: T).(arity g c t a0)) (let H11 \def (eq_ind_r nat i0 (\lambda
+(n: nat).(getl n c (CHead d1 (Bind Abbr) u0))) H3 i H9) in (let H12 \def
+(eq_ind C (CHead d (Bind Abbr) u) (\lambda (c0: C).(getl i c c0)) H0 (CHead
+d1 (Bind Abbr) u0) (getl_mono c (CHead d (Bind Abbr) u) i H0 (CHead d1 (Bind
+Abbr) u0) H11)) in (let H13 \def (f_equal C C (\lambda (e: C).(match e in C
+return (\lambda (_: C).C) with [(CSort _) \Rightarrow d | (CHead c0 _ _)
+\Rightarrow c0])) (CHead d (Bind Abbr) u) (CHead d1 (Bind Abbr) u0)
+(getl_mono c (CHead d (Bind Abbr) u) i H0 (CHead d1 (Bind Abbr) u0) H11)) in
+((let H14 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_:
+C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow t])) (CHead d
+(Bind Abbr) u) (CHead d1 (Bind Abbr) u0) (getl_mono c (CHead d (Bind Abbr) u)
+i H0 (CHead d1 (Bind Abbr) u0) H11)) in (\lambda (H15: (eq C d d1)).(let H16
+\def (eq_ind_r T u0 (\lambda (t: T).(getl i c (CHead d1 (Bind Abbr) t))) H12
+u H14) in (eq_ind T u (\lambda (t: T).(arity g c (lift (S i) O t) a0)) (let
+H17 \def (eq_ind_r C d1 (\lambda (c0: C).(getl i c (CHead c0 (Bind Abbr) u)))
+H16 d H15) in (arity_lift g d u a0 H1 c (S i) O (getl_drop Abbr c d u i
+H17))) u0 H14)))) H13)))) t2 H10))) (subst0_gen_lref u0 t2 i0 i H8)) c2 H7)))
+H6)) (\lambda (H6: (land (eq T (TLRef i) t2) (csubst0 i0 u0 c c2))).(and_ind
+(eq T (TLRef i) t2) (csubst0 i0 u0 c c2) (arity g c2 t2 a0) (\lambda (H7: (eq
+T (TLRef i) t2)).(\lambda (H8: (csubst0 i0 u0 c c2)).(eq_ind T (TLRef i)
+(\lambda (t: T).(arity g c2 t a0)) (lt_le_e i i0 (arity g c2 (TLRef i) a0)
+(\lambda (H9: (lt i i0)).(let H10 \def (csubst0_getl_lt i0 i H9 c c2 u0 H8
+(CHead d (Bind Abbr) u) H0) in (or4_ind (getl i c2 (CHead d (Bind Abbr) u))
+(ex3_4 B C T T (\lambda (b: B).(\lambda (e0: C).(\lambda (u1: T).(\lambda (_:
+T).(eq C (CHead d (Bind Abbr) u) (CHead e0 (Bind b) u1)))))) (\lambda (b:
+B).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(getl i c2 (CHead e0
+(Bind b) w)))))) (\lambda (_: B).(\lambda (_: C).(\lambda (u1: T).(\lambda
+(w: T).(subst0 (minus i0 (S i)) u0 u1 w)))))) (ex3_4 B C C T (\lambda (b: