+(c3: C).(\lambda (v0: T).(\lambda (a: A).(sc3 g (asucc g a) c3 v0))))
+(\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 (b: B).(\lambda (_: C).(\lambda (_: T).(eq K k (Bind
+b))))) (\lambda (b: B).(\lambda (_: C).(\lambda (_: T).(not (eq B b Void)))))
+(\lambda (_: B).(\lambda (c3: C).(\lambda (_: T).(csubc g c3 c2)))))))) H2 c2
+H8) in (let H10 \def (eq_ind C c0 (\lambda (c: C).(csubc g c1 c)) H1 c2 H8)
+in (or3_intro0 (ex2 C (\lambda (c3: C).(eq C (CHead c1 k w) (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 (v0:
+T).(\lambda (_: A).(eq C (CHead c1 k w) (CHead c3 (Bind Abst) v0)))))
+(\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g c3 c2)))) (\lambda
+(c3: C).(\lambda (v0: T).(\lambda (a: A).(sc3 g (asucc g a) c3 v0))))
+(\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 k w)
+(CHead c3 (Bind Void) v1))))) (\lambda (b: B).(\lambda (_: C).(\lambda (_:
+T).(eq K k (Bind b))))) (\lambda (b: B).(\lambda (_: C).(\lambda (_: T).(not
+(eq B b Void))))) (\lambda (_: B).(\lambda (c3: C).(\lambda (_: T).(csubc g
+c3 c2))))) (ex_intro2 C (\lambda (c3: C).(eq C (CHead c1 k w) (CHead c3 k
+w))) (\lambda (c3: C).(csubc g c3 c2)) c1 (refl_equal C (CHead c1 k w))
+H10)))) k0 H7) v H6)))) H5)) H4))))))))) (\lambda (c1: C).(\lambda (c0:
+C).(\lambda (H1: (csubc g c1 c0)).(\lambda (H2: (((eq C c0 (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 (b:
+B).(\lambda (_: C).(\lambda (_: T).(eq K k (Bind b))))) (\lambda (b:
+B).(\lambda (_: C).(\lambda (_: T).(not (eq B b Void))))) (\lambda (_:
+B).(\lambda (c3: C).(\lambda (_: T).(csubc g c3 c2))))))))).(\lambda (b:
+B).(\lambda (H3: (not (eq B b Void))).(\lambda (u1: T).(\lambda (u2:
+T).(\lambda (H4: (eq C (CHead c0 (Bind b) u2) (CHead c2 k w))).(let H5 \def
+(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 (_:
+C).(\lambda (_: T).(not (eq B b0 Void))))) (\lambda (_: B).(\lambda (c3:
+C).(\lambda (_: T).(csubc g c3 c2))))))) (or3_intro2 (ex2 C (\lambda (c3:
+C).(eq C (CHead c1 (Bind Void) u1) (CHead c3 (Bind b) w))) (\lambda (c3:
+C).(csubc g c3 c2))) (ex5_3 C T A (\lambda (_: C).(\lambda (_: T).(\lambda
+(_: A).(eq K (Bind b) (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 (Bind b) (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))))) (ex4_3_intro 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
+(Bind b) (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)))) b c1 u1 (refl_equal C (CHead c1 (Bind Void) u1)) (refl_equal K
+(Bind b)) H3 H11)) k H8))))))) H6)) H5))))))))))) (\lambda (c1: C).(\lambda
+(c0: C).(\lambda (H1: (csubc g c1 c0)).(\lambda (H2: (((eq C c0 (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 (b:
+B).(\lambda (_: C).(\lambda (_: T).(eq K k (Bind b))))) (\lambda (b:
+B).(\lambda (_: C).(\lambda (_: T).(not (eq B b Void))))) (\lambda (_:
+B).(\lambda (c3: C).(\lambda (_: T).(csubc g c3 c2))))))))).(\lambda (v: