-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))).(land_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
+Abbr) u0) H11)) in (let H13 \def (f_equal C C (\lambda (e: C).(match e 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 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))).(land_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_n (S i) (S i0) (le_S (S (S i)) (S i0)
+(le_n_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