-H2)) in ((let H5 \def (f_equal C T (\lambda (e: C).(match e in C return
-(\lambda (_: C).T) with [(CSort _) \Rightarrow v0 | (CHead _ _ t) \Rightarrow
-t])) (CHead d1 (Bind b1) v0) (CHead c3 (Bind Void) v1) (clear_gen_bind Void
-c3 (CHead d1 (Bind b1) v0) v1 H2)) in (\lambda (_: (eq B b1 Void)).(\lambda
-(H7: (eq C d1 c3)).(eq_ind_r C c3 (\lambda (c: C).(ex2_3 B C T (\lambda (_:
-B).(\lambda (d2: C).(\lambda (_: T).(csubv c d2)))) (\lambda (b2: B).(\lambda
-(d2: C).(\lambda (v3: T).(clear (CHead c4 (Bind Void) v2) (CHead d2 (Bind b2)
-v3))))))) (ex2_3_intro B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_:
-T).(csubv c3 d2)))) (\lambda (b2: B).(\lambda (d2: C).(\lambda (v3: T).(clear
-(CHead c4 (Bind Void) v2) (CHead d2 (Bind b2) v3))))) Void c4 v2 H0
-(clear_bind Void c4 v2)) d1 H7)))) H4)) H3)))))))))))) (\lambda (c3:
-C).(\lambda (c4: C).(\lambda (H0: (csubv c3 c4)).(\lambda (_: ((\forall (b1:
-B).(\forall (d1: C).(\forall (v1: T).((clear c3 (CHead d1 (Bind b1) v1)) \to
-(ex2_3 B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv d1
-d2)))) (\lambda (b2: B).(\lambda (d2: C).(\lambda (v2: T).(clear c4 (CHead d2
-(Bind b2) v2)))))))))))).(\lambda (b1: B).(\lambda (_: (not (eq B b1
-Void))).(\lambda (b2: B).(\lambda (v1: T).(\lambda (v2: T).(\lambda (b0:
-B).(\lambda (d1: C).(\lambda (v0: T).(\lambda (H3: (clear (CHead c3 (Bind b1)
-v1) (CHead d1 (Bind b0) v0))).(let H4 \def (f_equal C C (\lambda (e:
-C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d1 |
-(CHead c _ _) \Rightarrow c])) (CHead d1 (Bind b0) v0) (CHead c3 (Bind b1)
-v1) (clear_gen_bind b1 c3 (CHead d1 (Bind b0) v0) v1 H3)) in ((let H5 \def
-(f_equal C B (\lambda (e: C).(match e in C return (\lambda (_: C).B) with
-[(CSort _) \Rightarrow b0 | (CHead _ k _) \Rightarrow (match k in K return
-(\lambda (_: K).B) with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow
-b0])])) (CHead d1 (Bind b0) v0) (CHead c3 (Bind b1) v1) (clear_gen_bind b1 c3
-(CHead d1 (Bind b0) v0) v1 H3)) in ((let H6 \def (f_equal C T (\lambda (e:
-C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow v0 |
-(CHead _ _ t) \Rightarrow t])) (CHead d1 (Bind b0) v0) (CHead c3 (Bind b1)
-v1) (clear_gen_bind b1 c3 (CHead d1 (Bind b0) v0) v1 H3)) in (\lambda (_: (eq
-B b0 b1)).(\lambda (H8: (eq C d1 c3)).(eq_ind_r C c3 (\lambda (c: C).(ex2_3 B
-C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv c d2)))) (\lambda
+H2)) in ((let H4 \def (f_equal C B (\lambda (e: C).(match e with [(CSort _)
+\Rightarrow b1 | (CHead _ k _) \Rightarrow (match k with [(Bind b)
+\Rightarrow b | (Flat _) \Rightarrow b1])])) (CHead d1 (Bind b1) v0) (CHead
+c3 (Bind Void) v1) (clear_gen_bind Void c3 (CHead d1 (Bind b1) v0) v1 H2)) in
+((let H5 \def (f_equal C T (\lambda (e: C).(match e with [(CSort _)
+\Rightarrow v0 | (CHead _ _ t) \Rightarrow t])) (CHead d1 (Bind b1) v0)
+(CHead c3 (Bind Void) v1) (clear_gen_bind Void c3 (CHead d1 (Bind b1) v0) v1
+H2)) in (\lambda (_: (eq B b1 Void)).(\lambda (H7: (eq C d1 c3)).(eq_ind_r C
+c3 (\lambda (c: C).(ex2_3 B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_:
+T).(csubv c d2)))) (\lambda (b2: B).(\lambda (d2: C).(\lambda (v3: T).(clear
+(CHead c4 (Bind Void) v2) (CHead d2 (Bind b2) v3))))))) (ex2_3_intro B C T
+(\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv c3 d2)))) (\lambda
+(b2: B).(\lambda (d2: C).(\lambda (v3: T).(clear (CHead c4 (Bind Void) v2)
+(CHead d2 (Bind b2) v3))))) Void c4 v2 H0 (clear_bind Void c4 v2)) d1 H7))))
+H4)) H3)))))))))))) (\lambda (c3: C).(\lambda (c4: C).(\lambda (H0: (csubv c3
+c4)).(\lambda (_: ((\forall (b1: B).(\forall (d1: C).(\forall (v1: T).((clear
+c3 (CHead d1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (_: B).(\lambda (d2:
+C).(\lambda (_: T).(csubv d1 d2)))) (\lambda (b2: B).(\lambda (d2:
+C).(\lambda (v2: T).(clear c4 (CHead d2 (Bind b2) v2)))))))))))).(\lambda
+(b1: B).(\lambda (_: (not (eq B b1 Void))).(\lambda (b2: B).(\lambda (v1:
+T).(\lambda (v2: T).(\lambda (b0: B).(\lambda (d1: C).(\lambda (v0:
+T).(\lambda (H3: (clear (CHead c3 (Bind b1) v1) (CHead d1 (Bind b0)
+v0))).(let H4 \def (f_equal C C (\lambda (e: C).(match e with [(CSort _)
+\Rightarrow d1 | (CHead c _ _) \Rightarrow c])) (CHead d1 (Bind b0) v0)
+(CHead c3 (Bind b1) v1) (clear_gen_bind b1 c3 (CHead d1 (Bind b0) v0) v1 H3))
+in ((let H5 \def (f_equal C B (\lambda (e: C).(match e with [(CSort _)
+\Rightarrow b0 | (CHead _ k _) \Rightarrow (match k with [(Bind b)
+\Rightarrow b | (Flat _) \Rightarrow b0])])) (CHead d1 (Bind b0) v0) (CHead
+c3 (Bind b1) v1) (clear_gen_bind b1 c3 (CHead d1 (Bind b0) v0) v1 H3)) in
+((let H6 \def (f_equal C T (\lambda (e: C).(match e with [(CSort _)
+\Rightarrow v0 | (CHead _ _ t) \Rightarrow t])) (CHead d1 (Bind b0) v0)
+(CHead c3 (Bind b1) v1) (clear_gen_bind b1 c3 (CHead d1 (Bind b0) v0) v1 H3))
+in (\lambda (_: (eq B b0 b1)).(\lambda (H8: (eq C d1 c3)).(eq_ind_r C c3
+(\lambda (c: C).(ex2_3 B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_:
+T).(csubv c d2)))) (\lambda (b3: B).(\lambda (d2: C).(\lambda (v3: T).(clear
+(CHead c4 (Bind b2) v2) (CHead d2 (Bind b3) v3))))))) (ex2_3_intro B C T
+(\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv c3 d2)))) (\lambda