-u1))).(let H2 \def (eq_ind C (CSort n) (\lambda (ee: C).(match ee in C return
-(\lambda (_: C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _)
-\Rightarrow False])) I (CHead d1 (Flat f) u1) H1) in (False_ind (ex2_2 C T
-(\lambda (d2: C).(\lambda (u2: T).(eq C (CSort n) (CHead d2 (Flat f) u2))))
-(\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1)))) H2)))) (\lambda (c1:
-C).(\lambda (c2: C).(\lambda (H1: (csuba g c1 c2)).(\lambda (H2: (((eq C c2
-(CHead d1 (Flat f) u1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq
-C c1 (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
-d1))))))).(\lambda (k: K).(\lambda (u: T).(\lambda (H3: (eq C (CHead c2 k u)
-(CHead d1 (Flat f) u1))).(let H4 \def (f_equal C C (\lambda (e: C).(match e
-in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c2 | (CHead c0 _
-_) \Rightarrow c0])) (CHead c2 k u) (CHead d1 (Flat f) 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 c2 k
-u) (CHead d1 (Flat f) 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 c2 k u) (CHead d1 (Flat f) u1) H3) in
-(\lambda (H7: (eq K k (Flat f))).(\lambda (H8: (eq C c2 d1)).(eq_ind_r T u1
-(\lambda (t: T).(ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C (CHead c1
-k t) (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
-d1))))) (eq_ind_r K (Flat f) (\lambda (k0: K).(ex2_2 C T (\lambda (d2:
-C).(\lambda (u2: T).(eq C (CHead c1 k0 u1) (CHead d2 (Flat f) u2)))) (\lambda
-(d2: C).(\lambda (_: T).(csuba g d2 d1))))) (let H9 \def (eq_ind C c2
-(\lambda (c0: C).((eq C c0 (CHead d1 (Flat f) u1)) \to (ex2_2 C T (\lambda
-(d2: C).(\lambda (u2: T).(eq C c1 (CHead d2 (Flat f) u2)))) (\lambda (d2:
-C).(\lambda (_: T).(csuba g d2 d1)))))) H2 d1 H8) in (let H10 \def (eq_ind C
-c2 (\lambda (c0: C).(csuba g c1 c0)) H1 d1 H8) in (ex2_2_intro C T (\lambda
-(d2: C).(\lambda (u2: T).(eq C (CHead c1 (Flat f) u1) (CHead d2 (Flat f)
-u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))) c1 u1 (refl_equal C
-(CHead c1 (Flat f) u1)) H10))) k H7) u H6)))) H5)) H4))))))))) (\lambda (c1:
-C).(\lambda (c2: C).(\lambda (_: (csuba g c1 c2)).(\lambda (_: (((eq C c2
-(CHead d1 (Flat f) u1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq
-C c1 (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
-d1))))))).(\lambda (b: B).(\lambda (_: (not (eq B b Void))).(\lambda (u0:
-T).(\lambda (u2: T).(\lambda (H4: (eq C (CHead c2 (Bind b) u2) (CHead d1
-(Flat f) u1))).(let H5 \def (eq_ind C (CHead c2 (Bind b) u2) (\lambda (ee:
-C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow
-False | (CHead _ k _) \Rightarrow (match k in K return (\lambda (_: K).Prop)
-with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow False])])) I (CHead d1
-(Flat f) u1) H4) in (False_ind (ex2_2 C T (\lambda (d2: C).(\lambda (u3:
-T).(eq C (CHead c1 (Bind Void) u0) (CHead d2 (Flat f) u3)))) (\lambda (d2:
-C).(\lambda (_: T).(csuba g d2 d1)))) H5))))))))))) (\lambda (c1: C).(\lambda
-(c2: C).(\lambda (_: (csuba g c1 c2)).(\lambda (_: (((eq C c2 (CHead d1 (Flat
-f) u1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C c1 (CHead d2
+u1))).(let H2 \def (eq_ind C (CSort n) (\lambda (ee: C).(match ee with
+[(CSort _) \Rightarrow True | (CHead _ _ _) \Rightarrow False])) I (CHead d1
+(Flat f) u1) H1) in (False_ind (ex2_2 C T (\lambda (d2: C).(\lambda (u2:
+T).(eq C (CSort n) (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_:
+T).(csuba g d2 d1)))) H2)))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (H1:
+(csuba g c1 c2)).(\lambda (H2: (((eq C c2 (CHead d1 (Flat f) u1)) \to (ex2_2
+C T (\lambda (d2: C).(\lambda (u2: T).(eq C c1 (CHead d2 (Flat f) u2))))
+(\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))))).(\lambda (k:
+K).(\lambda (u: T).(\lambda (H3: (eq C (CHead c2 k u) (CHead d1 (Flat f)
+u1))).(let H4 \def (f_equal C C (\lambda (e: C).(match e with [(CSort _)
+\Rightarrow c2 | (CHead c0 _ _) \Rightarrow c0])) (CHead c2 k u) (CHead d1
+(Flat f) u1) H3) in ((let H5 \def (f_equal C K (\lambda (e: C).(match e with
+[(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0])) (CHead c2 k u)
+(CHead d1 (Flat f) u1) H3) in ((let H6 \def (f_equal C T (\lambda (e:
+C).(match e with [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow t]))
+(CHead c2 k u) (CHead d1 (Flat f) u1) H3) in (\lambda (H7: (eq K k (Flat
+f))).(\lambda (H8: (eq C c2 d1)).(eq_ind_r T u1 (\lambda (t: T).(ex2_2 C T
+(\lambda (d2: C).(\lambda (u2: T).(eq C (CHead c1 k t) (CHead d2 (Flat f)
+u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))) (eq_ind_r K (Flat
+f) (\lambda (k0: K).(ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C (CHead
+c1 k0 u1) (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g
+d2 d1))))) (let H9 \def (eq_ind C c2 (\lambda (c0: C).((eq C c0 (CHead d1
+(Flat f) u1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C c1
+(CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
+d1)))))) H2 d1 H8) in (let H10 \def (eq_ind C c2 (\lambda (c0: C).(csuba g c1
+c0)) H1 d1 H8) in (ex2_2_intro C T (\lambda (d2: C).(\lambda (u2: T).(eq C
+(CHead c1 (Flat f) u1) (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda
+(_: T).(csuba g d2 d1))) c1 u1 (refl_equal C (CHead c1 (Flat f) u1)) H10))) k
+H7) u H6)))) H5)) H4))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (_:
+(csuba g c1 c2)).(\lambda (_: (((eq C c2 (CHead d1 (Flat f) u1)) \to (ex2_2 C
+T (\lambda (d2: C).(\lambda (u2: T).(eq C c1 (CHead d2 (Flat f) u2))))
+(\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))))).(\lambda (b:
+B).(\lambda (_: (not (eq B b Void))).(\lambda (u0: T).(\lambda (u2:
+T).(\lambda (H4: (eq C (CHead c2 (Bind b) u2) (CHead d1 (Flat f) u1))).(let
+H5 \def (eq_ind C (CHead c2 (Bind b) u2) (\lambda (ee: C).(match ee with
+[(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match k with [(Bind
+_) \Rightarrow True | (Flat _) \Rightarrow False])])) I (CHead d1 (Flat f)
+u1) H4) in (False_ind (ex2_2 C T (\lambda (d2: C).(\lambda (u3: T).(eq C
+(CHead c1 (Bind Void) u0) (CHead d2 (Flat f) u3)))) (\lambda (d2: C).(\lambda
+(_: T).(csuba g d2 d1)))) H5))))))))))) (\lambda (c1: C).(\lambda (c2:
+C).(\lambda (_: (csuba g c1 c2)).(\lambda (_: (((eq C c2 (CHead d1 (Flat f)
+u1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C c1 (CHead d2