- \lambda (c1: C).(\lambda (c2: C).(\lambda (v: T).(\lambda (i: nat).(\lambda
-(H: (csubst0 i v c1 c2)).(csubst0_ind (\lambda (n: nat).(\lambda (t:
-T).(\lambda (c: C).(\lambda (c0: C).(\forall (e2: C).((clear c0 e2) \to (or
-(clear c e2) (ex2 C (\lambda (e1: C).(csubst0 n t e1 e2)) (\lambda (e1:
-C).(clear c e1)))))))))) (\lambda (k: K).(\lambda (i0: nat).(\lambda (v0:
-T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (H0: (subst0 i0 v0 u1
-u2)).(\lambda (c: C).(\lambda (e2: C).(\lambda (H1: (clear (CHead c k u2)
-e2)).(K_ind (\lambda (k0: K).((clear (CHead c k0 u2) e2) \to (or (clear
-(CHead c k0 u1) e2) (ex2 C (\lambda (e1: C).(csubst0 (s k0 i0) v0 e1 e2))
-(\lambda (e1: C).(clear (CHead c k0 u1) e1)))))) (\lambda (b: B).(\lambda
-(H2: (clear (CHead c (Bind b) u2) e2)).(eq_ind_r C (CHead c (Bind b) u2)
-(\lambda (c0: C).(or (clear (CHead c (Bind b) u1) c0) (ex2 C (\lambda (e1:
-C).(csubst0 (s (Bind b) i0) v0 e1 c0)) (\lambda (e1: C).(clear (CHead c (Bind
-b) u1) e1))))) (or_intror (clear (CHead c (Bind b) u1) (CHead c (Bind b) u2))
-(ex2 C (\lambda (e1: C).(csubst0 (S i0) v0 e1 (CHead c (Bind b) u2)))
-(\lambda (e1: C).(clear (CHead c (Bind b) u1) e1))) (ex_intro2 C (\lambda
-(e1: C).(csubst0 (S i0) v0 e1 (CHead c (Bind b) u2))) (\lambda (e1: C).(clear
-(CHead c (Bind b) u1) e1)) (CHead c (Bind b) u1) (csubst0_snd_bind b i0 v0 u1
-u2 H0 c) (clear_bind b c u1))) e2 (clear_gen_bind b c e2 u2 H2)))) (\lambda
-(f: F).(\lambda (H2: (clear (CHead c (Flat f) u2) e2)).(or_introl (clear
-(CHead c (Flat f) u1) e2) (ex2 C (\lambda (e1: C).(csubst0 i0 v0 e1 e2))
-(\lambda (e1: C).(clear (CHead c (Flat f) u1) e1))) (clear_flat c e2
-(clear_gen_flat f c e2 u2 H2) f u1)))) k H1)))))))))) (\lambda (k:
-K).(\lambda (i0: nat).(\lambda (c3: C).(\lambda (c4: C).(\lambda (v0:
-T).(\lambda (H0: (csubst0 i0 v0 c3 c4)).(\lambda (H1: ((\forall (e2:
-C).((clear c4 e2) \to (or (clear c3 e2) (ex2 C (\lambda (e1: C).(csubst0 i0
-v0 e1 e2)) (\lambda (e1: C).(clear c3 e1)))))))).(\lambda (u: T).(\lambda
-(e2: C).(\lambda (H2: (clear (CHead c4 k u) e2)).(K_ind (\lambda (k0:
-K).((clear (CHead c4 k0 u) e2) \to (or (clear (CHead c3 k0 u) e2) (ex2 C
-(\lambda (e1: C).(csubst0 (s k0 i0) v0 e1 e2)) (\lambda (e1: C).(clear (CHead
-c3 k0 u) e1)))))) (\lambda (b: B).(\lambda (H3: (clear (CHead c4 (Bind b) u)
-e2)).(eq_ind_r C (CHead c4 (Bind b) u) (\lambda (c: C).(or (clear (CHead c3
-(Bind b) u) c) (ex2 C (\lambda (e1: C).(csubst0 (s (Bind b) i0) v0 e1 c))
-(\lambda (e1: C).(clear (CHead c3 (Bind b) u) e1))))) (or_intror (clear
-(CHead c3 (Bind b) u) (CHead c4 (Bind b) u)) (ex2 C (\lambda (e1: C).(csubst0
-(S i0) v0 e1 (CHead c4 (Bind b) u))) (\lambda (e1: C).(clear (CHead c3 (Bind
-b) u) e1))) (ex_intro2 C (\lambda (e1: C).(csubst0 (S i0) v0 e1 (CHead c4
-(Bind b) u))) (\lambda (e1: C).(clear (CHead c3 (Bind b) u) e1)) (CHead c3
-(Bind b) u) (csubst0_fst_bind b i0 c3 c4 v0 H0 u) (clear_bind b c3 u))) e2
-(clear_gen_bind b c4 e2 u H3)))) (\lambda (f: F).(\lambda (H3: (clear (CHead
-c4 (Flat f) u) e2)).(let H_x \def (H1 e2 (clear_gen_flat f c4 e2 u H3)) in
-(let H4 \def H_x in (or_ind (clear c3 e2) (ex2 C (\lambda (e1: C).(csubst0 i0
-v0 e1 e2)) (\lambda (e1: C).(clear c3 e1))) (or (clear (CHead c3 (Flat f) u)
-e2) (ex2 C (\lambda (e1: C).(csubst0 i0 v0 e1 e2)) (\lambda (e1: C).(clear
-(CHead c3 (Flat f) u) e1)))) (\lambda (H5: (clear c3 e2)).(or_introl (clear
-(CHead c3 (Flat f) u) e2) (ex2 C (\lambda (e1: C).(csubst0 i0 v0 e1 e2))
-(\lambda (e1: C).(clear (CHead c3 (Flat f) u) e1))) (clear_flat c3 e2 H5 f
-u))) (\lambda (H5: (ex2 C (\lambda (e1: C).(csubst0 i0 v0 e1 e2)) (\lambda
-(e1: C).(clear c3 e1)))).(ex2_ind C (\lambda (e1: C).(csubst0 i0 v0 e1 e2))
-(\lambda (e1: C).(clear c3 e1)) (or (clear (CHead c3 (Flat f) u) e2) (ex2 C
-(\lambda (e1: C).(csubst0 i0 v0 e1 e2)) (\lambda (e1: C).(clear (CHead c3
-(Flat f) u) e1)))) (\lambda (x: C).(\lambda (H6: (csubst0 i0 v0 x
-e2)).(\lambda (H7: (clear c3 x)).(or_intror (clear (CHead c3 (Flat f) u) e2)
-(ex2 C (\lambda (e1: C).(csubst0 i0 v0 e1 e2)) (\lambda (e1: C).(clear (CHead
-c3 (Flat f) u) e1))) (ex_intro2 C (\lambda (e1: C).(csubst0 i0 v0 e1 e2))
-(\lambda (e1: C).(clear (CHead c3 (Flat f) u) e1)) x H6 (clear_flat c3 x H7 f
-u)))))) H5)) H4))))) k H2))))))))))) (\lambda (k: K).(\lambda (i0:
-nat).(\lambda (v0: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (H0: (subst0
-i0 v0 u1 u2)).(\lambda (c3: C).(\lambda (c4: C).(\lambda (H1: (csubst0 i0 v0
-c3 c4)).(\lambda (H2: ((\forall (e2: C).((clear c4 e2) \to (or (clear c3 e2)
-(ex2 C (\lambda (e1: C).(csubst0 i0 v0 e1 e2)) (\lambda (e1: C).(clear c3
-e1)))))))).(\lambda (e2: C).(\lambda (H3: (clear (CHead c4 k u2) e2)).(K_ind
-(\lambda (k0: K).((clear (CHead c4 k0 u2) e2) \to (or (clear (CHead c3 k0 u1)
-e2) (ex2 C (\lambda (e1: C).(csubst0 (s k0 i0) v0 e1 e2)) (\lambda (e1:
-C).(clear (CHead c3 k0 u1) e1)))))) (\lambda (b: B).(\lambda (H4: (clear
-(CHead c4 (Bind b) u2) e2)).(eq_ind_r C (CHead c4 (Bind b) u2) (\lambda (c:
-C).(or (clear (CHead c3 (Bind b) u1) c) (ex2 C (\lambda (e1: C).(csubst0 (s
-(Bind b) i0) v0 e1 c)) (\lambda (e1: C).(clear (CHead c3 (Bind b) u1) e1)))))
-(or_intror (clear (CHead c3 (Bind b) u1) (CHead c4 (Bind b) u2)) (ex2 C
-(\lambda (e1: C).(csubst0 (S i0) v0 e1 (CHead c4 (Bind b) u2))) (\lambda (e1:
-C).(clear (CHead c3 (Bind b) u1) e1))) (ex_intro2 C (\lambda (e1: C).(csubst0
-(S i0) v0 e1 (CHead c4 (Bind b) u2))) (\lambda (e1: C).(clear (CHead c3 (Bind
-b) u1) e1)) (CHead c3 (Bind b) u1) (csubst0_both_bind b i0 v0 u1 u2 H0 c3 c4
-H1) (clear_bind b c3 u1))) e2 (clear_gen_bind b c4 e2 u2 H4)))) (\lambda (f:
-F).(\lambda (H4: (clear (CHead c4 (Flat f) u2) e2)).(let H_x \def (H2 e2
-(clear_gen_flat f c4 e2 u2 H4)) in (let H5 \def H_x in (or_ind (clear c3 e2)
-(ex2 C (\lambda (e1: C).(csubst0 i0 v0 e1 e2)) (\lambda (e1: C).(clear c3
-e1))) (or (clear (CHead c3 (Flat f) u1) e2) (ex2 C (\lambda (e1: C).(csubst0
-i0 v0 e1 e2)) (\lambda (e1: C).(clear (CHead c3 (Flat f) u1) e1)))) (\lambda
-(H6: (clear c3 e2)).(or_introl (clear (CHead c3 (Flat f) u1) e2) (ex2 C
-(\lambda (e1: C).(csubst0 i0 v0 e1 e2)) (\lambda (e1: C).(clear (CHead c3
-(Flat f) u1) e1))) (clear_flat c3 e2 H6 f u1))) (\lambda (H6: (ex2 C (\lambda
-(e1: C).(csubst0 i0 v0 e1 e2)) (\lambda (e1: C).(clear c3 e1)))).(ex2_ind C
-(\lambda (e1: C).(csubst0 i0 v0 e1 e2)) (\lambda (e1: C).(clear c3 e1)) (or
-(clear (CHead c3 (Flat f) u1) e2) (ex2 C (\lambda (e1: C).(csubst0 i0 v0 e1
-e2)) (\lambda (e1: C).(clear (CHead c3 (Flat f) u1) e1)))) (\lambda (x:
-C).(\lambda (H7: (csubst0 i0 v0 x e2)).(\lambda (H8: (clear c3 x)).(or_intror
-(clear (CHead c3 (Flat f) u1) e2) (ex2 C (\lambda (e1: C).(csubst0 i0 v0 e1
-e2)) (\lambda (e1: C).(clear (CHead c3 (Flat f) u1) e1))) (ex_intro2 C
-(\lambda (e1: C).(csubst0 i0 v0 e1 e2)) (\lambda (e1: C).(clear (CHead c3
-(Flat f) u1) e1)) x H7 (clear_flat c3 x H8 f u1)))))) H6)) H5))))) k
-H3))))))))))))) i v c1 c2 H))))).
-(* COMMENTS
-Initial nodes: 2085
-END *)
+ \lambda (c1: C).(C_ind (\lambda (c: C).(\forall (c2: C).(\forall (v:
+T).(\forall (i: nat).((csubst0 i v c c2) \to (\forall (e2: C).((clear c2 e2)
+\to (or (clear c e2) (ex2 C (\lambda (e1: C).(csubst0 i v e1 e2)) (\lambda
+(e1: C).(clear c e1))))))))))) (\lambda (n: nat).(\lambda (c2: C).(\lambda
+(v: T).(\lambda (i: nat).(\lambda (H: (csubst0 i v (CSort n) c2)).(\lambda
+(e2: C).(\lambda (_: (clear c2 e2)).(csubst0_gen_sort c2 v i n H (or (clear
+(CSort n) e2) (ex2 C (\lambda (e1: C).(csubst0 i v e1 e2)) (\lambda (e1:
+C).(clear (CSort n) e1)))))))))))) (\lambda (c: C).(\lambda (H: ((\forall
+(c2: C).(\forall (v: T).(\forall (i: nat).((csubst0 i v c c2) \to (\forall
+(e2: C).((clear c2 e2) \to (or (clear c e2) (ex2 C (\lambda (e1: C).(csubst0
+i v e1 e2)) (\lambda (e1: C).(clear c e1)))))))))))).(\lambda (k: K).(\lambda
+(t: T).(\lambda (c2: C).(\lambda (v: T).(\lambda (i: nat).(\lambda (H0:
+(csubst0 i v (CHead c k t) c2)).(\lambda (e2: C).(\lambda (H1: (clear c2
+e2)).(let H2 \def (csubst0_gen_head k c c2 t v i H0) in (or3_ind (ex3_2 T nat
+(\lambda (_: T).(\lambda (j: nat).(eq nat i (s k j)))) (\lambda (u2:
+T).(\lambda (_: nat).(eq C c2 (CHead c k u2)))) (\lambda (u2: T).(\lambda (j:
+nat).(subst0 j v t u2)))) (ex3_2 C nat (\lambda (_: C).(\lambda (j: nat).(eq
+nat i (s k j)))) (\lambda (c3: C).(\lambda (_: nat).(eq C c2 (CHead c3 k
+t)))) (\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c c3)))) (ex4_3 T C nat
+(\lambda (_: T).(\lambda (_: C).(\lambda (j: nat).(eq nat i (s k j)))))
+(\lambda (u2: T).(\lambda (c3: C).(\lambda (_: nat).(eq C c2 (CHead c3 k
+u2))))) (\lambda (u2: T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v t
+u2)))) (\lambda (_: T).(\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c
+c3))))) (or (clear (CHead c k t) e2) (ex2 C (\lambda (e1: C).(csubst0 i v e1
+e2)) (\lambda (e1: C).(clear (CHead c k t) e1)))) (\lambda (H3: (ex3_2 T nat
+(\lambda (_: T).(\lambda (j: nat).(eq nat i (s k j)))) (\lambda (u2:
+T).(\lambda (_: nat).(eq C c2 (CHead c k u2)))) (\lambda (u2: T).(\lambda (j:
+nat).(subst0 j v t u2))))).(ex3_2_ind T nat (\lambda (_: T).(\lambda (j:
+nat).(eq nat i (s k j)))) (\lambda (u2: T).(\lambda (_: nat).(eq C c2 (CHead
+c k u2)))) (\lambda (u2: T).(\lambda (j: nat).(subst0 j v t u2))) (or (clear
+(CHead c k t) e2) (ex2 C (\lambda (e1: C).(csubst0 i v e1 e2)) (\lambda (e1:
+C).(clear (CHead c k t) e1)))) (\lambda (x0: T).(\lambda (x1: nat).(\lambda
+(H4: (eq nat i (s k x1))).(\lambda (H5: (eq C c2 (CHead c k x0))).(\lambda
+(H6: (subst0 x1 v t x0)).(eq_ind_r nat (s k x1) (\lambda (n: nat).(or (clear
+(CHead c k t) e2) (ex2 C (\lambda (e1: C).(csubst0 n v e1 e2)) (\lambda (e1:
+C).(clear (CHead c k t) e1))))) (let H7 \def (eq_ind C c2 (\lambda (c0:
+C).(clear c0 e2)) H1 (CHead c k x0) H5) in (K_ind (\lambda (k0: K).((clear
+(CHead c k0 x0) e2) \to (or (clear (CHead c k0 t) e2) (ex2 C (\lambda (e1:
+C).(csubst0 (s k0 x1) v e1 e2)) (\lambda (e1: C).(clear (CHead c k0 t)
+e1)))))) (\lambda (b: B).(\lambda (H8: (clear (CHead c (Bind b) x0)
+e2)).(eq_ind_r C (CHead c (Bind b) x0) (\lambda (c0: C).(or (clear (CHead c
+(Bind b) t) c0) (ex2 C (\lambda (e1: C).(csubst0 (s (Bind b) x1) v e1 c0))
+(\lambda (e1: C).(clear (CHead c (Bind b) t) e1))))) (or_intror (clear (CHead
+c (Bind b) t) (CHead c (Bind b) x0)) (ex2 C (\lambda (e1: C).(csubst0 (s
+(Bind b) x1) v e1 (CHead c (Bind b) x0))) (\lambda (e1: C).(clear (CHead c
+(Bind b) t) e1))) (ex_intro2 C (\lambda (e1: C).(csubst0 (s (Bind b) x1) v e1
+(CHead c (Bind b) x0))) (\lambda (e1: C).(clear (CHead c (Bind b) t) e1))
+(CHead c (Bind b) t) (csubst0_snd (Bind b) x1 v t x0 H6 c) (clear_bind b c
+t))) e2 (clear_gen_bind b c e2 x0 H8)))) (\lambda (f: F).(\lambda (H8: (clear
+(CHead c (Flat f) x0) e2)).(or_introl (clear (CHead c (Flat f) t) e2) (ex2 C
+(\lambda (e1: C).(csubst0 (s (Flat f) x1) v e1 e2)) (\lambda (e1: C).(clear
+(CHead c (Flat f) t) e1))) (clear_flat c e2 (clear_gen_flat f c e2 x0 H8) f
+t)))) k H7)) i H4)))))) H3)) (\lambda (H3: (ex3_2 C nat (\lambda (_:
+C).(\lambda (j: nat).(eq nat i (s k j)))) (\lambda (c3: C).(\lambda (_:
+nat).(eq C c2 (CHead c3 k t)))) (\lambda (c3: C).(\lambda (j: nat).(csubst0 j
+v c c3))))).(ex3_2_ind C nat (\lambda (_: C).(\lambda (j: nat).(eq nat i (s k
+j)))) (\lambda (c3: C).(\lambda (_: nat).(eq C c2 (CHead c3 k t)))) (\lambda
+(c3: C).(\lambda (j: nat).(csubst0 j v c c3))) (or (clear (CHead c k t) e2)
+(ex2 C (\lambda (e1: C).(csubst0 i v e1 e2)) (\lambda (e1: C).(clear (CHead c
+k t) e1)))) (\lambda (x0: C).(\lambda (x1: nat).(\lambda (H4: (eq nat i (s k
+x1))).(\lambda (H5: (eq C c2 (CHead x0 k t))).(\lambda (H6: (csubst0 x1 v c
+x0)).(eq_ind_r nat (s k x1) (\lambda (n: nat).(or (clear (CHead c k t) e2)
+(ex2 C (\lambda (e1: C).(csubst0 n v e1 e2)) (\lambda (e1: C).(clear (CHead c
+k t) e1))))) (let H7 \def (eq_ind C c2 (\lambda (c0: C).(clear c0 e2)) H1
+(CHead x0 k t) H5) in (K_ind (\lambda (k0: K).((clear (CHead x0 k0 t) e2) \to
+(or (clear (CHead c k0 t) e2) (ex2 C (\lambda (e1: C).(csubst0 (s k0 x1) v e1
+e2)) (\lambda (e1: C).(clear (CHead c k0 t) e1)))))) (\lambda (b: B).(\lambda
+(H8: (clear (CHead x0 (Bind b) t) e2)).(eq_ind_r C (CHead x0 (Bind b) t)
+(\lambda (c0: C).(or (clear (CHead c (Bind b) t) c0) (ex2 C (\lambda (e1:
+C).(csubst0 (s (Bind b) x1) v e1 c0)) (\lambda (e1: C).(clear (CHead c (Bind
+b) t) e1))))) (or_intror (clear (CHead c (Bind b) t) (CHead x0 (Bind b) t))
+(ex2 C (\lambda (e1: C).(csubst0 (s (Bind b) x1) v e1 (CHead x0 (Bind b) t)))
+(\lambda (e1: C).(clear (CHead c (Bind b) t) e1))) (ex_intro2 C (\lambda (e1:
+C).(csubst0 (s (Bind b) x1) v e1 (CHead x0 (Bind b) t))) (\lambda (e1:
+C).(clear (CHead c (Bind b) t) e1)) (CHead c (Bind b) t) (csubst0_fst (Bind
+b) x1 c x0 v H6 t) (clear_bind b c t))) e2 (clear_gen_bind b x0 e2 t H8))))
+(\lambda (f: F).(\lambda (H8: (clear (CHead x0 (Flat f) t) e2)).(let H_x \def
+(H x0 v x1 H6 e2 (clear_gen_flat f x0 e2 t H8)) in (let H9 \def H_x in
+(or_ind (clear c e2) (ex2 C (\lambda (e1: C).(csubst0 x1 v e1 e2)) (\lambda
+(e1: C).(clear c e1))) (or (clear (CHead c (Flat f) t) e2) (ex2 C (\lambda
+(e1: C).(csubst0 (s (Flat f) x1) v e1 e2)) (\lambda (e1: C).(clear (CHead c
+(Flat f) t) e1)))) (\lambda (H10: (clear c e2)).(or_introl (clear (CHead c
+(Flat f) t) e2) (ex2 C (\lambda (e1: C).(csubst0 (s (Flat f) x1) v e1 e2))
+(\lambda (e1: C).(clear (CHead c (Flat f) t) e1))) (clear_flat c e2 H10 f
+t))) (\lambda (H10: (ex2 C (\lambda (e1: C).(csubst0 x1 v e1 e2)) (\lambda
+(e1: C).(clear c e1)))).(ex2_ind C (\lambda (e1: C).(csubst0 x1 v e1 e2))
+(\lambda (e1: C).(clear c e1)) (or (clear (CHead c (Flat f) t) e2) (ex2 C
+(\lambda (e1: C).(csubst0 (s (Flat f) x1) v e1 e2)) (\lambda (e1: C).(clear
+(CHead c (Flat f) t) e1)))) (\lambda (x: C).(\lambda (H11: (csubst0 x1 v x
+e2)).(\lambda (H12: (clear c x)).(or_intror (clear (CHead c (Flat f) t) e2)
+(ex2 C (\lambda (e1: C).(csubst0 (s (Flat f) x1) v e1 e2)) (\lambda (e1:
+C).(clear (CHead c (Flat f) t) e1))) (ex_intro2 C (\lambda (e1: C).(csubst0
+(s (Flat f) x1) v e1 e2)) (\lambda (e1: C).(clear (CHead c (Flat f) t) e1)) x
+H11 (clear_flat c x H12 f t)))))) H10)) H9))))) k H7)) i H4)))))) H3))
+(\lambda (H3: (ex4_3 T C nat (\lambda (_: T).(\lambda (_: C).(\lambda (j:
+nat).(eq nat i (s k j))))) (\lambda (u2: T).(\lambda (c3: C).(\lambda (_:
+nat).(eq C c2 (CHead c3 k u2))))) (\lambda (u2: T).(\lambda (_: C).(\lambda
+(j: nat).(subst0 j v t u2)))) (\lambda (_: T).(\lambda (c3: C).(\lambda (j:
+nat).(csubst0 j v c c3)))))).(ex4_3_ind T C nat (\lambda (_: T).(\lambda (_:
+C).(\lambda (j: nat).(eq nat i (s k j))))) (\lambda (u2: T).(\lambda (c3:
+C).(\lambda (_: nat).(eq C c2 (CHead c3 k u2))))) (\lambda (u2: T).(\lambda
+(_: C).(\lambda (j: nat).(subst0 j v t u2)))) (\lambda (_: T).(\lambda (c3:
+C).(\lambda (j: nat).(csubst0 j v c c3)))) (or (clear (CHead c k t) e2) (ex2
+C (\lambda (e1: C).(csubst0 i v e1 e2)) (\lambda (e1: C).(clear (CHead c k t)
+e1)))) (\lambda (x0: T).(\lambda (x1: C).(\lambda (x2: nat).(\lambda (H4: (eq
+nat i (s k x2))).(\lambda (H5: (eq C c2 (CHead x1 k x0))).(\lambda (H6:
+(subst0 x2 v t x0)).(\lambda (H7: (csubst0 x2 v c x1)).(eq_ind_r nat (s k x2)
+(\lambda (n: nat).(or (clear (CHead c k t) e2) (ex2 C (\lambda (e1:
+C).(csubst0 n v e1 e2)) (\lambda (e1: C).(clear (CHead c k t) e1))))) (let H8
+\def (eq_ind C c2 (\lambda (c0: C).(clear c0 e2)) H1 (CHead x1 k x0) H5) in
+(K_ind (\lambda (k0: K).((clear (CHead x1 k0 x0) e2) \to (or (clear (CHead c
+k0 t) e2) (ex2 C (\lambda (e1: C).(csubst0 (s k0 x2) v e1 e2)) (\lambda (e1:
+C).(clear (CHead c k0 t) e1)))))) (\lambda (b: B).(\lambda (H9: (clear (CHead
+x1 (Bind b) x0) e2)).(eq_ind_r C (CHead x1 (Bind b) x0) (\lambda (c0: C).(or
+(clear (CHead c (Bind b) t) c0) (ex2 C (\lambda (e1: C).(csubst0 (s (Bind b)
+x2) v e1 c0)) (\lambda (e1: C).(clear (CHead c (Bind b) t) e1))))) (or_intror
+(clear (CHead c (Bind b) t) (CHead x1 (Bind b) x0)) (ex2 C (\lambda (e1:
+C).(csubst0 (s (Bind b) x2) v e1 (CHead x1 (Bind b) x0))) (\lambda (e1:
+C).(clear (CHead c (Bind b) t) e1))) (ex_intro2 C (\lambda (e1: C).(csubst0
+(s (Bind b) x2) v e1 (CHead x1 (Bind b) x0))) (\lambda (e1: C).(clear (CHead
+c (Bind b) t) e1)) (CHead c (Bind b) t) (csubst0_both (Bind b) x2 v t x0 H6 c
+x1 H7) (clear_bind b c t))) e2 (clear_gen_bind b x1 e2 x0 H9)))) (\lambda (f:
+F).(\lambda (H9: (clear (CHead x1 (Flat f) x0) e2)).(let H_x \def (H x1 v x2
+H7 e2 (clear_gen_flat f x1 e2 x0 H9)) in (let H10 \def H_x in (or_ind (clear
+c e2) (ex2 C (\lambda (e1: C).(csubst0 x2 v e1 e2)) (\lambda (e1: C).(clear c
+e1))) (or (clear (CHead c (Flat f) t) e2) (ex2 C (\lambda (e1: C).(csubst0 (s
+(Flat f) x2) v e1 e2)) (\lambda (e1: C).(clear (CHead c (Flat f) t) e1))))
+(\lambda (H11: (clear c e2)).(or_introl (clear (CHead c (Flat f) t) e2) (ex2
+C (\lambda (e1: C).(csubst0 (s (Flat f) x2) v e1 e2)) (\lambda (e1: C).(clear
+(CHead c (Flat f) t) e1))) (clear_flat c e2 H11 f t))) (\lambda (H11: (ex2 C
+(\lambda (e1: C).(csubst0 x2 v e1 e2)) (\lambda (e1: C).(clear c
+e1)))).(ex2_ind C (\lambda (e1: C).(csubst0 x2 v e1 e2)) (\lambda (e1:
+C).(clear c e1)) (or (clear (CHead c (Flat f) t) e2) (ex2 C (\lambda (e1:
+C).(csubst0 (s (Flat f) x2) v e1 e2)) (\lambda (e1: C).(clear (CHead c (Flat
+f) t) e1)))) (\lambda (x: C).(\lambda (H12: (csubst0 x2 v x e2)).(\lambda
+(H13: (clear c x)).(or_intror (clear (CHead c (Flat f) t) e2) (ex2 C (\lambda
+(e1: C).(csubst0 (s (Flat f) x2) v e1 e2)) (\lambda (e1: C).(clear (CHead c
+(Flat f) t) e1))) (ex_intro2 C (\lambda (e1: C).(csubst0 (s (Flat f) x2) v e1
+e2)) (\lambda (e1: C).(clear (CHead c (Flat f) t) e1)) x H12 (clear_flat c x
+H13 f t)))))) H11)) H10))))) k H8)) i H4)))))))) H3)) H2)))))))))))) c1).