-A).(arity g d2 u2 a)))))))) (\lambda (H9: (csuba g d1 c2)).(or_introl (ex2 C
-(\lambda (d2: C).(eq C (CHead c2 (Bind Abst) u1) (CHead d2 (Bind Abst) u1)))
-(\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda
-(u2: T).(\lambda (_: A).(eq C (CHead c2 (Bind Abst) u1) (CHead d2 (Bind Abbr)
-u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
-(\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
-a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
-a))))) (ex_intro2 C (\lambda (d2: C).(eq C (CHead c2 (Bind Abst) u1) (CHead
-d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)) c2 (refl_equal C
-(CHead c2 (Bind Abst) u1)) H9))) c H8)) u (sym_eq T u u1 H7))) k (sym_eq K k
-(Bind Abst) H6))) c1 (sym_eq C c1 d1 H5))) H4)) H3)) H2 H0))) | (csuba_abst
-c1 c2 H0 t a H1 u H2) \Rightarrow (\lambda (H3: (eq C (CHead c1 (Bind Abst)
-t) (CHead d1 (Bind Abst) u1))).(\lambda (H4: (eq C (CHead c2 (Bind Abbr) u)
-c)).((let H5 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda
-(_: C).T) with [(CSort _) \Rightarrow t | (CHead _ _ t0) \Rightarrow t0]))
-(CHead c1 (Bind Abst) t) (CHead d1 (Bind Abst) u1) H3) in ((let H6 \def
-(f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with
-[(CSort _) \Rightarrow c1 | (CHead c0 _ _) \Rightarrow c0])) (CHead c1 (Bind
-Abst) t) (CHead d1 (Bind Abst) u1) H3) in (eq_ind C d1 (\lambda (c0: C).((eq
-T t u1) \to ((eq C (CHead c2 (Bind Abbr) u) c) \to ((csuba g c0 c2) \to
-((arity g c0 t (asucc g a)) \to ((arity g c2 u a) \to (or (ex2 C (\lambda
-(d2: C).(eq C c (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1
-d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c
-(CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
-A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(arity
-g d1 u1 (asucc g a0))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a0:
-A).(arity g d2 u2 a0)))))))))))) (\lambda (H7: (eq T t u1)).(eq_ind T u1
-(\lambda (t0: T).((eq C (CHead c2 (Bind Abbr) u) c) \to ((csuba g d1 c2) \to
-((arity g d1 t0 (asucc g a)) \to ((arity g c2 u a) \to (or (ex2 C (\lambda
-(d2: C).(eq C c (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1
-d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c
-(CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
-A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(arity
-g d1 u1 (asucc g a0))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a0:
-A).(arity g d2 u2 a0))))))))))) (\lambda (H8: (eq C (CHead c2 (Bind Abbr) u)
-c)).(eq_ind C (CHead c2 (Bind Abbr) u) (\lambda (c0: C).((csuba g d1 c2) \to
-((arity g d1 u1 (asucc g a)) \to ((arity g c2 u a) \to (or (ex2 C (\lambda
-(d2: C).(eq C c0 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1
-d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c0
-(CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
-A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(arity
-g d1 u1 (asucc g a0))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a0:
-A).(arity g d2 u2 a0)))))))))) (\lambda (H9: (csuba g d1 c2)).(\lambda (H10:
-(arity g d1 u1 (asucc g a))).(\lambda (H11: (arity g c2 u a)).(or_intror (ex2
-C (\lambda (d2: C).(eq C (CHead c2 (Bind Abbr) u) (CHead d2 (Bind Abst) u1)))
-(\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda
+A).(arity g d2 u2 a))))))))).(\lambda (k: K).(\lambda (u: T).(\lambda (H3:
+(eq C (CHead c1 k u) (CHead d1 (Bind Abst) u1))).(let H4 \def (f_equal C C
+(\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _)
+\Rightarrow c1 | (CHead c0 _ _) \Rightarrow c0])) (CHead c1 k u) (CHead d1
+(Bind Abst) u1) H3) in ((let H5 \def (f_equal C K (\lambda (e: C).(match e in
+C return (\lambda (_: C).K) with [(CSort _) \Rightarrow k | (CHead _ k0 _)
+\Rightarrow k0])) (CHead c1 k u) (CHead d1 (Bind Abst) u1) H3) in ((let H6
+\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 c1 k u)
+(CHead d1 (Bind Abst) u1) H3) in (\lambda (H7: (eq K k (Bind Abst))).(\lambda
+(H8: (eq C c1 d1)).(eq_ind_r T u1 (\lambda (t: T).(or (ex2 C (\lambda (d2:
+C).(eq C (CHead c2 k t) (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g
+d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C
+(CHead c2 k t) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
+T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
+T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
+(u2: T).(\lambda (a: A).(arity g d2 u2 a))))))) (eq_ind_r K (Bind Abst)
+(\lambda (k0: K).(or (ex2 C (\lambda (d2: C).(eq C (CHead c2 k0 u1) (CHead d2
+(Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda
+(d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C (CHead c2 k0 u1) (CHead d2
+(Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
+d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
+(asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2
+u2 a))))))) (let H9 \def (eq_ind C c1 (\lambda (c0: C).((eq C c0 (CHead d1
+(Bind Abst) u1)) \to (or (ex2 C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind
+Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
+C).(\lambda (u2: T).(\lambda (_: A).(eq C c2 (CHead d2 (Bind Abbr) u2)))))
+(\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
+(_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a)))))
+(\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))))) H2
+d1 H8) in (let H10 \def (eq_ind C c1 (\lambda (c0: C).(csuba g c0 c2)) H1 d1
+H8) in (or_introl (ex2 C (\lambda (d2: C).(eq C (CHead c2 (Bind Abst) u1)
+(CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A
+(\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C (CHead c2 (Bind Abst)
+u1) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
+(_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a:
+A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda
+(a: A).(arity g d2 u2 a))))) (ex_intro2 C (\lambda (d2: C).(eq C (CHead c2
+(Bind Abst) u1) (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))
+c2 (refl_equal C (CHead c2 (Bind Abst) u1)) H10)))) k H7) u H6)))) H5))
+H4))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: (csuba g c1
+c2)).(\lambda (H2: (((eq C c1 (CHead d1 (Bind Abst) u1)) \to (or (ex2 C
+(\lambda (d2: C).(eq C c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba
+g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq
+C c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
+(_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a:
+A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda
+(a: A).(arity g d2 u2 a))))))))).(\lambda (t: T).(\lambda (a: A).(\lambda
+(H3: (arity g c1 t (asucc g a))).(\lambda (u: T).(\lambda (H4: (arity g c2 u
+a)).(\lambda (H5: (eq C (CHead c1 (Bind Abst) t) (CHead d1 (Bind Abst)
+u1))).(let H6 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda
+(_: C).C) with [(CSort _) \Rightarrow c1 | (CHead c0 _ _) \Rightarrow c0]))
+(CHead c1 (Bind Abst) t) (CHead d1 (Bind Abst) u1) H5) in ((let H7 \def
+(f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with
+[(CSort _) \Rightarrow t | (CHead _ _ t0) \Rightarrow t0])) (CHead c1 (Bind
+Abst) t) (CHead d1 (Bind Abst) u1) H5) in (\lambda (H8: (eq C c1 d1)).(let H9
+\def (eq_ind T t (\lambda (t0: T).(arity g c1 t0 (asucc g a))) H3 u1 H7) in
+(let H10 \def (eq_ind C c1 (\lambda (c0: C).(arity g c0 u1 (asucc g a))) H9
+d1 H8) in (let H11 \def (eq_ind C c1 (\lambda (c0: C).((eq C c0 (CHead d1
+(Bind Abst) u1)) \to (or (ex2 C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind
+Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
+C).(\lambda (u2: T).(\lambda (_: A).(eq C c2 (CHead d2 (Bind Abbr) u2)))))
+(\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
+(_: C).(\lambda (_: T).(\lambda (a0: A).(arity g d1 u1 (asucc g a0)))))
+(\lambda (d2: C).(\lambda (u2: T).(\lambda (a0: A).(arity g d2 u2 a0))))))))
+H2 d1 H8) in (let H12 \def (eq_ind C c1 (\lambda (c0: C).(csuba g c0 c2)) H1
+d1 H8) in (or_intror (ex2 C (\lambda (d2: C).(eq C (CHead c2 (Bind Abbr) u)
+(CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A
+(\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C (CHead c2 (Bind Abbr)
+u) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
+(_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0:
+A).(arity g d1 u1 (asucc g a0))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda
+(a0: A).(arity g d2 u2 a0))))) (ex4_3_intro C T A (\lambda (d2: C).(\lambda