-(f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with
-[(CSort _) \Rightarrow c0 | (CHead c _ _) \Rightarrow c])) (CHead c0 (Bind b)
-u2) (CHead c2 k w) H4) in ((let H6 \def (f_equal C K (\lambda (e: C).(match e
-in C return (\lambda (_: C).K) with [(CSort _) \Rightarrow (Bind b) | (CHead
-_ k0 _) \Rightarrow k0])) (CHead c0 (Bind b) u2) (CHead c2 k w) H4) in ((let
-H7 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T)
-with [(CSort _) \Rightarrow u2 | (CHead _ _ t) \Rightarrow t])) (CHead c0
-(Bind b) u2) (CHead c2 k w) H4) in (\lambda (H8: (eq K (Bind b) k)).(\lambda
-(H9: (eq C c0 c2)).(let H10 \def (eq_ind C c0 (\lambda (c: C).((eq C c (CHead
-c2 k w)) \to (or3 (ex2 C (\lambda (c3: C).(eq C c1 (CHead c3 k w))) (\lambda
-(c3: C).(csubc g c3 c2))) (ex5_3 C T A (\lambda (_: C).(\lambda (_:
-T).(\lambda (_: A).(eq K k (Bind Abbr))))) (\lambda (c3: C).(\lambda (v:
-T).(\lambda (_: A).(eq C c1 (CHead c3 (Bind Abst) v))))) (\lambda (c3:
-C).(\lambda (_: T).(\lambda (_: A).(csubc g c3 c2)))) (\lambda (c3:
-C).(\lambda (v: T).(\lambda (a: A).(sc3 g (asucc g a) c3 v)))) (\lambda (_:
-C).(\lambda (_: T).(\lambda (a: A).(sc3 g a c2 w))))) (ex4_3 B C T (\lambda
-(_: B).(\lambda (c3: C).(\lambda (v1: T).(eq C c1 (CHead c3 (Bind Void)
-v1))))) (\lambda (b0: B).(\lambda (_: C).(\lambda (_: T).(eq K k (Bind
-b0))))) (\lambda (b0: B).(\lambda (_: C).(\lambda (_: T).(not (eq B b0
-Void))))) (\lambda (_: B).(\lambda (c3: C).(\lambda (_: T).(csubc g c3
-c2)))))))) H2 c2 H9) in (let H11 \def (eq_ind C c0 (\lambda (c: C).(csubc g
-c1 c)) H1 c2 H9) in (let H12 \def (eq_ind_r K k (\lambda (k0: K).((eq C c2
-(CHead c2 k0 w)) \to (or3 (ex2 C (\lambda (c3: C).(eq C c1 (CHead c3 k0 w)))
-(\lambda (c3: C).(csubc g c3 c2))) (ex5_3 C T A (\lambda (_: C).(\lambda (_:
-T).(\lambda (_: A).(eq K k0 (Bind Abbr))))) (\lambda (c3: C).(\lambda (v:
-T).(\lambda (_: A).(eq C c1 (CHead c3 (Bind Abst) v))))) (\lambda (c3:
-C).(\lambda (_: T).(\lambda (_: A).(csubc g c3 c2)))) (\lambda (c3:
-C).(\lambda (v: T).(\lambda (a: A).(sc3 g (asucc g a) c3 v)))) (\lambda (_:
-C).(\lambda (_: T).(\lambda (a: A).(sc3 g a c2 w))))) (ex4_3 B C T (\lambda
-(_: B).(\lambda (c3: C).(\lambda (v1: T).(eq C c1 (CHead c3 (Bind Void)
-v1))))) (\lambda (b0: B).(\lambda (_: C).(\lambda (_: T).(eq K k0 (Bind
-b0))))) (\lambda (b0: B).(\lambda (_: C).(\lambda (_: T).(not (eq B b0
-Void))))) (\lambda (_: B).(\lambda (c3: C).(\lambda (_: T).(csubc g c3
-c2)))))))) H10 (Bind b) H8) in (eq_ind K (Bind b) (\lambda (k0: K).(or3 (ex2
-C (\lambda (c3: C).(eq C (CHead c1 (Bind Void) u1) (CHead c3 k0 w))) (\lambda
-(c3: C).(csubc g c3 c2))) (ex5_3 C T A (\lambda (_: C).(\lambda (_:
-T).(\lambda (_: A).(eq K k0 (Bind Abbr))))) (\lambda (c3: C).(\lambda (v:
-T).(\lambda (_: A).(eq C (CHead c1 (Bind Void) u1) (CHead c3 (Bind Abst)
-v))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g c3 c2))))
-(\lambda (c3: C).(\lambda (v: T).(\lambda (a: A).(sc3 g (asucc g a) c3 v))))
-(\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g a c2 w))))) (ex4_3 B C
-T (\lambda (_: B).(\lambda (c3: C).(\lambda (v1: T).(eq C (CHead c1 (Bind
-Void) u1) (CHead c3 (Bind Void) v1))))) (\lambda (b0: B).(\lambda (_:
-C).(\lambda (_: T).(eq K k0 (Bind b0))))) (\lambda (b0: B).(\lambda (_:
+(f_equal C C (\lambda (e: C).(match e with [(CSort _) \Rightarrow c0 | (CHead
+c _ _) \Rightarrow c])) (CHead c0 (Bind b) u2) (CHead c2 k w) H4) in ((let H6
+\def (f_equal C K (\lambda (e: C).(match e with [(CSort _) \Rightarrow (Bind
+b) | (CHead _ k0 _) \Rightarrow k0])) (CHead c0 (Bind b) u2) (CHead c2 k w)
+H4) in ((let H7 \def (f_equal C T (\lambda (e: C).(match e with [(CSort _)
+\Rightarrow u2 | (CHead _ _ t) \Rightarrow t])) (CHead c0 (Bind b) u2) (CHead
+c2 k w) H4) in (\lambda (H8: (eq K (Bind b) k)).(\lambda (H9: (eq C c0
+c2)).(let H10 \def (eq_ind C c0 (\lambda (c: C).((eq C c (CHead c2 k w)) \to
+(or3 (ex2 C (\lambda (c3: C).(eq C c1 (CHead c3 k w))) (\lambda (c3:
+C).(csubc g c3 c2))) (ex5_3 C T A (\lambda (_: C).(\lambda (_: T).(\lambda
+(_: A).(eq K k (Bind Abbr))))) (\lambda (c3: C).(\lambda (v: T).(\lambda (_:
+A).(eq C c1 (CHead c3 (Bind Abst) v))))) (\lambda (c3: C).(\lambda (_:
+T).(\lambda (_: A).(csubc g c3 c2)))) (\lambda (c3: C).(\lambda (v:
+T).(\lambda (a: A).(sc3 g (asucc g a) c3 v)))) (\lambda (_: C).(\lambda (_:
+T).(\lambda (a: A).(sc3 g a c2 w))))) (ex4_3 B C T (\lambda (_: B).(\lambda
+(c3: C).(\lambda (v1: T).(eq C c1 (CHead c3 (Bind Void) v1))))) (\lambda (b0:
+B).(\lambda (_: C).(\lambda (_: T).(eq K k (Bind b0))))) (\lambda (b0:
+B).(\lambda (_: C).(\lambda (_: T).(not (eq B b0 Void))))) (\lambda (_:
+B).(\lambda (c3: C).(\lambda (_: T).(csubc g c3 c2)))))))) H2 c2 H9) in (let
+H11 \def (eq_ind C c0 (\lambda (c: C).(csubc g c1 c)) H1 c2 H9) in (let H12
+\def (eq_ind_r K k (\lambda (k0: K).((eq C c2 (CHead c2 k0 w)) \to (or3 (ex2
+C (\lambda (c3: C).(eq C c1 (CHead c3 k0 w))) (\lambda (c3: C).(csubc g c3
+c2))) (ex5_3 C T A (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k0
+(Bind Abbr))))) (\lambda (c3: C).(\lambda (v: T).(\lambda (_: A).(eq C c1
+(CHead c3 (Bind Abst) v))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_:
+A).(csubc g c3 c2)))) (\lambda (c3: C).(\lambda (v: T).(\lambda (a: A).(sc3 g
+(asucc g a) c3 v)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g a
+c2 w))))) (ex4_3 B C T (\lambda (_: B).(\lambda (c3: C).(\lambda (v1: T).(eq
+C c1 (CHead c3 (Bind Void) v1))))) (\lambda (b0: B).(\lambda (_: C).(\lambda
+(_: T).(eq K k0 (Bind b0))))) (\lambda (b0: B).(\lambda (_: C).(\lambda (_:
+T).(not (eq B b0 Void))))) (\lambda (_: B).(\lambda (c3: C).(\lambda (_:
+T).(csubc g c3 c2)))))))) H10 (Bind b) H8) in (eq_ind K (Bind b) (\lambda
+(k0: K).(or3 (ex2 C (\lambda (c3: C).(eq C (CHead c1 (Bind Void) u1) (CHead
+c3 k0 w))) (\lambda (c3: C).(csubc g c3 c2))) (ex5_3 C T A (\lambda (_:
+C).(\lambda (_: T).(\lambda (_: A).(eq K k0 (Bind Abbr))))) (\lambda (c3:
+C).(\lambda (v: T).(\lambda (_: A).(eq C (CHead c1 (Bind Void) u1) (CHead c3
+(Bind Abst) v))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g
+c3 c2)))) (\lambda (c3: C).(\lambda (v: T).(\lambda (a: A).(sc3 g (asucc g a)
+c3 v)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g a c2 w)))))
+(ex4_3 B C T (\lambda (_: B).(\lambda (c3: C).(\lambda (v1: T).(eq C (CHead
+c1 (Bind Void) u1) (CHead c3 (Bind Void) v1))))) (\lambda (b0: B).(\lambda
+(_: C).(\lambda (_: T).(eq K k0 (Bind b0))))) (\lambda (b0: B).(\lambda (_: