H15)))))))))) H14)) H13)))))))) k H3 (drop_gen_drop k x1 e x0 n0 H7))))))))))
H2)) (csubst0_gen_head k c c2 t v (S n0) H0))))))))))) c1)))) n).
+theorem csubst0_drop_lt_back:
+ \forall (n: nat).(\forall (i: nat).((lt n i) \to (\forall (c1: C).(\forall
+(c2: C).(\forall (v: T).((csubst0 i v c1 c2) \to (\forall (e2: C).((drop n O
+c2 e2) \to (or (drop n O c1 e2) (ex2 C (\lambda (e1: C).(csubst0 (minus i n)
+v e1 e2)) (\lambda (e1: C).(drop n O c1 e1))))))))))))
+\def
+ \lambda (n: nat).(nat_ind (\lambda (n0: nat).(\forall (i: nat).((lt n0 i)
+\to (\forall (c1: C).(\forall (c2: C).(\forall (v: T).((csubst0 i v c1 c2)
+\to (\forall (e2: C).((drop n0 O c2 e2) \to (or (drop n0 O c1 e2) (ex2 C
+(\lambda (e1: C).(csubst0 (minus i n0) v e1 e2)) (\lambda (e1: C).(drop n0 O
+c1 e1))))))))))))) (\lambda (i: nat).(\lambda (_: (lt O i)).(\lambda (c1:
+C).(\lambda (c2: C).(\lambda (v: T).(\lambda (H0: (csubst0 i v c1
+c2)).(\lambda (e2: C).(\lambda (H1: (drop O O c2 e2)).(eq_ind C c2 (\lambda
+(c: C).(or (drop O O c1 c) (ex2 C (\lambda (e1: C).(csubst0 (minus i O) v e1
+c)) (\lambda (e1: C).(drop O O c1 e1))))) (eq_ind nat i (\lambda (n0:
+nat).(or (drop O O c1 c2) (ex2 C (\lambda (e1: C).(csubst0 n0 v e1 c2))
+(\lambda (e1: C).(drop O O c1 e1))))) (or_intror (drop O O c1 c2) (ex2 C
+(\lambda (e1: C).(csubst0 i v e1 c2)) (\lambda (e1: C).(drop O O c1 e1)))
+(ex_intro2 C (\lambda (e1: C).(csubst0 i v e1 c2)) (\lambda (e1: C).(drop O O
+c1 e1)) c1 H0 (drop_refl c1))) (minus i O) (minus_n_O i)) e2 (drop_gen_refl
+c2 e2 H1)))))))))) (\lambda (n0: nat).(\lambda (IHn: ((\forall (i: nat).((lt
+n0 i) \to (\forall (c1: C).(\forall (c2: C).(\forall (v: T).((csubst0 i v c1
+c2) \to (\forall (e2: C).((drop n0 O c2 e2) \to (or (drop n0 O c1 e2) (ex2 C
+(\lambda (e1: C).(csubst0 (minus i n0) v e1 e2)) (\lambda (e1: C).(drop n0 O
+c1 e1)))))))))))))).(\lambda (i: nat).(\lambda (H: (lt (S n0) i)).(\lambda
+(c1: C).(C_ind (\lambda (c: C).(\forall (c2: C).(\forall (v: T).((csubst0 i v
+c c2) \to (\forall (e2: C).((drop (S n0) O c2 e2) \to (or (drop (S n0) O c
+e2) (ex2 C (\lambda (e1: C).(csubst0 (minus i (S n0)) v e1 e2)) (\lambda (e1:
+C).(drop (S n0) O c e1)))))))))) (\lambda (n1: nat).(\lambda (c2: C).(\lambda
+(v: T).(\lambda (H0: (csubst0 i v (CSort n1) c2)).(\lambda (e2: C).(\lambda
+(_: (drop (S n0) O c2 e2)).(csubst0_gen_sort c2 v i n1 H0 (or (drop (S n0) O
+(CSort n1) e2) (ex2 C (\lambda (e1: C).(csubst0 (minus i (S n0)) v e1 e2))
+(\lambda (e1: C).(drop (S n0) O (CSort n1) e1))))))))))) (\lambda (c:
+C).(\lambda (H0: ((\forall (c2: C).(\forall (v: T).((csubst0 i v c c2) \to
+(\forall (e2: C).((drop (S n0) O c2 e2) \to (or (drop (S n0) O c e2) (ex2 C
+(\lambda (e1: C).(csubst0 (minus i (S n0)) v e1 e2)) (\lambda (e1: C).(drop
+(S n0) O c e1))))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (c2:
+C).(\lambda (v: T).(\lambda (H1: (csubst0 i v (CHead c k t) c2)).(\lambda
+(e2: C).(\lambda (H2: (drop (S n0) O c2 e2)).(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 (drop (S n0)
+O (CHead c k t) e2) (ex2 C (\lambda (e1: C).(csubst0 (minus i (S n0)) v e1
+e2)) (\lambda (e1: C).(drop (S n0) O (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 (drop (S n0) O (CHead c k t) e2) (ex2 C (\lambda (e1:
+C).(csubst0 (minus i (S n0)) v e1 e2)) (\lambda (e1: C).(drop (S n0) O (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 (_: (subst0 x1 v t
+x0)).(let H7 \def (eq_ind C c2 (\lambda (c0: C).(drop (S n0) O c0 e2)) H2
+(CHead c k x0) H5) in (let H8 \def (eq_ind nat i (\lambda (n1: nat).(\forall
+(c3: C).(\forall (v0: T).((csubst0 n1 v0 c c3) \to (\forall (e3: C).((drop (S
+n0) O c3 e3) \to (or (drop (S n0) O c e3) (ex2 C (\lambda (e1: C).(csubst0
+(minus n1 (S n0)) v0 e1 e3)) (\lambda (e1: C).(drop (S n0) O c e1))))))))))
+H0 (s k x1) H4) in (let H9 \def (eq_ind nat i (\lambda (n1: nat).(lt (S n0)
+n1)) H (s k x1) H4) in (eq_ind_r nat (s k x1) (\lambda (n1: nat).(or (drop (S
+n0) O (CHead c k t) e2) (ex2 C (\lambda (e1: C).(csubst0 (minus n1 (S n0)) v
+e1 e2)) (\lambda (e1: C).(drop (S n0) O (CHead c k t) e1))))) (K_ind (\lambda
+(k0: K).(((\forall (c3: C).(\forall (v0: T).((csubst0 (s k0 x1) v0 c c3) \to
+(\forall (e3: C).((drop (S n0) O c3 e3) \to (or (drop (S n0) O c e3) (ex2 C
+(\lambda (e1: C).(csubst0 (minus (s k0 x1) (S n0)) v0 e1 e3)) (\lambda (e1:
+C).(drop (S n0) O c e1)))))))))) \to ((lt (S n0) (s k0 x1)) \to ((drop (r k0
+n0) O c e2) \to (or (drop (S n0) O (CHead c k0 t) e2) (ex2 C (\lambda (e1:
+C).(csubst0 (minus (s k0 x1) (S n0)) v e1 e2)) (\lambda (e1: C).(drop (S n0)
+O (CHead c k0 t) e1)))))))) (\lambda (b: B).(\lambda (_: ((\forall (c3:
+C).(\forall (v0: T).((csubst0 (s (Bind b) x1) v0 c c3) \to (\forall (e3:
+C).((drop (S n0) O c3 e3) \to (or (drop (S n0) O c e3) (ex2 C (\lambda (e1:
+C).(csubst0 (minus (s (Bind b) x1) (S n0)) v0 e1 e3)) (\lambda (e1: C).(drop
+(S n0) O c e1))))))))))).(\lambda (_: (lt (S n0) (s (Bind b) x1))).(\lambda
+(H12: (drop (r (Bind b) n0) O c e2)).(or_introl (drop (S n0) O (CHead c (Bind
+b) t) e2) (ex2 C (\lambda (e1: C).(csubst0 (minus x1 n0) v e1 e2)) (\lambda
+(e1: C).(drop (S n0) O (CHead c (Bind b) t) e1))) (drop_drop (Bind b) n0 c e2
+H12 t)))))) (\lambda (f: F).(\lambda (_: ((\forall (c3: C).(\forall (v0:
+T).((csubst0 (s (Flat f) x1) v0 c c3) \to (\forall (e3: C).((drop (S n0) O c3
+e3) \to (or (drop (S n0) O c e3) (ex2 C (\lambda (e1: C).(csubst0 (minus (s
+(Flat f) x1) (S n0)) v0 e1 e3)) (\lambda (e1: C).(drop (S n0) O c
+e1))))))))))).(\lambda (_: (lt (S n0) (s (Flat f) x1))).(\lambda (H12: (drop
+(r (Flat f) n0) O c e2)).(or_introl (drop (S n0) O (CHead c (Flat f) t) e2)
+(ex2 C (\lambda (e1: C).(csubst0 (minus x1 (S n0)) v e1 e2)) (\lambda (e1:
+C).(drop (S n0) O (CHead c (Flat f) t) e1))) (drop_drop (Flat f) n0 c e2 H12
+t)))))) k H8 H9 (drop_gen_drop k c e2 x0 n0 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 (drop (S n0) O (CHead c k t) e2) (ex2 C (\lambda (e1:
+C).(csubst0 (minus i (S n0)) v e1 e2)) (\lambda (e1: C).(drop (S n0) O (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)).(let H7 \def (eq_ind C c2 (\lambda (c0: C).(drop (S n0) O c0 e2)) H2
+(CHead x0 k t) H5) in (let H8 \def (eq_ind nat i (\lambda (n1: nat).(\forall
+(c3: C).(\forall (v0: T).((csubst0 n1 v0 c c3) \to (\forall (e3: C).((drop (S
+n0) O c3 e3) \to (or (drop (S n0) O c e3) (ex2 C (\lambda (e1: C).(csubst0
+(minus n1 (S n0)) v0 e1 e3)) (\lambda (e1: C).(drop (S n0) O c e1))))))))))
+H0 (s k x1) H4) in (let H9 \def (eq_ind nat i (\lambda (n1: nat).(lt (S n0)
+n1)) H (s k x1) H4) in (eq_ind_r nat (s k x1) (\lambda (n1: nat).(or (drop (S
+n0) O (CHead c k t) e2) (ex2 C (\lambda (e1: C).(csubst0 (minus n1 (S n0)) v
+e1 e2)) (\lambda (e1: C).(drop (S n0) O (CHead c k t) e1))))) (K_ind (\lambda
+(k0: K).(((\forall (c3: C).(\forall (v0: T).((csubst0 (s k0 x1) v0 c c3) \to
+(\forall (e3: C).((drop (S n0) O c3 e3) \to (or (drop (S n0) O c e3) (ex2 C
+(\lambda (e1: C).(csubst0 (minus (s k0 x1) (S n0)) v0 e1 e3)) (\lambda (e1:
+C).(drop (S n0) O c e1)))))))))) \to ((lt (S n0) (s k0 x1)) \to ((drop (r k0
+n0) O x0 e2) \to (or (drop (S n0) O (CHead c k0 t) e2) (ex2 C (\lambda (e1:
+C).(csubst0 (minus (s k0 x1) (S n0)) v e1 e2)) (\lambda (e1: C).(drop (S n0)
+O (CHead c k0 t) e1)))))))) (\lambda (b: B).(\lambda (_: ((\forall (c3:
+C).(\forall (v0: T).((csubst0 (s (Bind b) x1) v0 c c3) \to (\forall (e3:
+C).((drop (S n0) O c3 e3) \to (or (drop (S n0) O c e3) (ex2 C (\lambda (e1:
+C).(csubst0 (minus (s (Bind b) x1) (S n0)) v0 e1 e3)) (\lambda (e1: C).(drop
+(S n0) O c e1))))))))))).(\lambda (H11: (lt (S n0) (s (Bind b) x1))).(\lambda
+(H12: (drop (r (Bind b) n0) O x0 e2)).(let H_x \def (IHn x1 (lt_S_n n0 x1
+H11) c x0 v H6 e2 H12) in (let H13 \def H_x in (or_ind (drop n0 O c e2) (ex2
+C (\lambda (e1: C).(csubst0 (minus x1 n0) v e1 e2)) (\lambda (e1: C).(drop n0
+O c e1))) (or (drop (S n0) O (CHead c (Bind b) t) e2) (ex2 C (\lambda (e1:
+C).(csubst0 (minus x1 n0) v e1 e2)) (\lambda (e1: C).(drop (S n0) O (CHead c
+(Bind b) t) e1)))) (\lambda (H14: (drop n0 O c e2)).(or_introl (drop (S n0) O
+(CHead c (Bind b) t) e2) (ex2 C (\lambda (e1: C).(csubst0 (minus x1 n0) v e1
+e2)) (\lambda (e1: C).(drop (S n0) O (CHead c (Bind b) t) e1))) (drop_drop
+(Bind b) n0 c e2 H14 t))) (\lambda (H14: (ex2 C (\lambda (e1: C).(csubst0
+(minus x1 n0) v e1 e2)) (\lambda (e1: C).(drop n0 O c e1)))).(ex2_ind C
+(\lambda (e1: C).(csubst0 (minus x1 n0) v e1 e2)) (\lambda (e1: C).(drop n0 O
+c e1)) (or (drop (S n0) O (CHead c (Bind b) t) e2) (ex2 C (\lambda (e1:
+C).(csubst0 (minus x1 n0) v e1 e2)) (\lambda (e1: C).(drop (S n0) O (CHead c
+(Bind b) t) e1)))) (\lambda (x: C).(\lambda (H15: (csubst0 (minus x1 n0) v x
+e2)).(\lambda (H16: (drop n0 O c x)).(or_intror (drop (S n0) O (CHead c (Bind
+b) t) e2) (ex2 C (\lambda (e1: C).(csubst0 (minus x1 n0) v e1 e2)) (\lambda
+(e1: C).(drop (S n0) O (CHead c (Bind b) t) e1))) (ex_intro2 C (\lambda (e1:
+C).(csubst0 (minus x1 n0) v e1 e2)) (\lambda (e1: C).(drop (S n0) O (CHead c
+(Bind b) t) e1)) x H15 (drop_drop (Bind b) n0 c x H16 t)))))) H14))
+H13))))))) (\lambda (f: F).(\lambda (H10: ((\forall (c3: C).(\forall (v0:
+T).((csubst0 (s (Flat f) x1) v0 c c3) \to (\forall (e3: C).((drop (S n0) O c3
+e3) \to (or (drop (S n0) O c e3) (ex2 C (\lambda (e1: C).(csubst0 (minus (s
+(Flat f) x1) (S n0)) v0 e1 e3)) (\lambda (e1: C).(drop (S n0) O c
+e1))))))))))).(\lambda (_: (lt (S n0) (s (Flat f) x1))).(\lambda (H12: (drop
+(r (Flat f) n0) O x0 e2)).(let H_x \def (H10 x0 v H6 e2 H12) in (let H13 \def
+H_x in (or_ind (drop (S n0) O c e2) (ex2 C (\lambda (e1: C).(csubst0 (minus
+x1 (S n0)) v e1 e2)) (\lambda (e1: C).(drop (S n0) O c e1))) (or (drop (S n0)
+O (CHead c (Flat f) t) e2) (ex2 C (\lambda (e1: C).(csubst0 (minus x1 (S n0))
+v e1 e2)) (\lambda (e1: C).(drop (S n0) O (CHead c (Flat f) t) e1))))
+(\lambda (H14: (drop (S n0) O c e2)).(or_introl (drop (S n0) O (CHead c (Flat
+f) t) e2) (ex2 C (\lambda (e1: C).(csubst0 (minus x1 (S n0)) v e1 e2))
+(\lambda (e1: C).(drop (S n0) O (CHead c (Flat f) t) e1))) (drop_drop (Flat
+f) n0 c e2 H14 t))) (\lambda (H14: (ex2 C (\lambda (e1: C).(csubst0 (minus x1
+(S n0)) v e1 e2)) (\lambda (e1: C).(drop (S n0) O c e1)))).(ex2_ind C
+(\lambda (e1: C).(csubst0 (minus x1 (S n0)) v e1 e2)) (\lambda (e1: C).(drop
+(S n0) O c e1)) (or (drop (S n0) O (CHead c (Flat f) t) e2) (ex2 C (\lambda
+(e1: C).(csubst0 (minus x1 (S n0)) v e1 e2)) (\lambda (e1: C).(drop (S n0) O
+(CHead c (Flat f) t) e1)))) (\lambda (x: C).(\lambda (H15: (csubst0 (minus x1
+(S n0)) v x e2)).(\lambda (H16: (drop (S n0) O c x)).(or_intror (drop (S n0)
+O (CHead c (Flat f) t) e2) (ex2 C (\lambda (e1: C).(csubst0 (minus x1 (S n0))
+v e1 e2)) (\lambda (e1: C).(drop (S n0) O (CHead c (Flat f) t) e1)))
+(ex_intro2 C (\lambda (e1: C).(csubst0 (minus x1 (S n0)) v e1 e2)) (\lambda
+(e1: C).(drop (S n0) O (CHead c (Flat f) t) e1)) x H15 (drop_drop (Flat f) n0
+c x H16 t)))))) H14)) H13))))))) k H8 H9 (drop_gen_drop k x0 e2 t n0 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 (drop (S n0)
+O (CHead c k t) e2) (ex2 C (\lambda (e1: C).(csubst0 (minus i (S n0)) v e1
+e2)) (\lambda (e1: C).(drop (S n0) O (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 (_: (subst0 x2 v t
+x0)).(\lambda (H7: (csubst0 x2 v c x1)).(let H8 \def (eq_ind C c2 (\lambda
+(c0: C).(drop (S n0) O c0 e2)) H2 (CHead x1 k x0) H5) in (let H9 \def (eq_ind
+nat i (\lambda (n1: nat).(\forall (c3: C).(\forall (v0: T).((csubst0 n1 v0 c
+c3) \to (\forall (e3: C).((drop (S n0) O c3 e3) \to (or (drop (S n0) O c e3)
+(ex2 C (\lambda (e1: C).(csubst0 (minus n1 (S n0)) v0 e1 e3)) (\lambda (e1:
+C).(drop (S n0) O c e1)))))))))) H0 (s k x2) H4) in (let H10 \def (eq_ind nat
+i (\lambda (n1: nat).(lt (S n0) n1)) H (s k x2) H4) in (eq_ind_r nat (s k x2)
+(\lambda (n1: nat).(or (drop (S n0) O (CHead c k t) e2) (ex2 C (\lambda (e1:
+C).(csubst0 (minus n1 (S n0)) v e1 e2)) (\lambda (e1: C).(drop (S n0) O
+(CHead c k t) e1))))) (K_ind (\lambda (k0: K).(((\forall (c3: C).(\forall
+(v0: T).((csubst0 (s k0 x2) v0 c c3) \to (\forall (e3: C).((drop (S n0) O c3
+e3) \to (or (drop (S n0) O c e3) (ex2 C (\lambda (e1: C).(csubst0 (minus (s
+k0 x2) (S n0)) v0 e1 e3)) (\lambda (e1: C).(drop (S n0) O c e1)))))))))) \to
+((lt (S n0) (s k0 x2)) \to ((drop (r k0 n0) O x1 e2) \to (or (drop (S n0) O
+(CHead c k0 t) e2) (ex2 C (\lambda (e1: C).(csubst0 (minus (s k0 x2) (S n0))
+v e1 e2)) (\lambda (e1: C).(drop (S n0) O (CHead c k0 t) e1)))))))) (\lambda
+(b: B).(\lambda (_: ((\forall (c3: C).(\forall (v0: T).((csubst0 (s (Bind b)
+x2) v0 c c3) \to (\forall (e3: C).((drop (S n0) O c3 e3) \to (or (drop (S n0)
+O c e3) (ex2 C (\lambda (e1: C).(csubst0 (minus (s (Bind b) x2) (S n0)) v0 e1
+e3)) (\lambda (e1: C).(drop (S n0) O c e1))))))))))).(\lambda (H12: (lt (S
+n0) (s (Bind b) x2))).(\lambda (H13: (drop (r (Bind b) n0) O x1 e2)).(let H_x
+\def (IHn x2 (lt_S_n n0 x2 H12) c x1 v H7 e2 H13) in (let H14 \def H_x in
+(or_ind (drop n0 O c e2) (ex2 C (\lambda (e1: C).(csubst0 (minus x2 n0) v e1
+e2)) (\lambda (e1: C).(drop n0 O c e1))) (or (drop (S n0) O (CHead c (Bind b)
+t) e2) (ex2 C (\lambda (e1: C).(csubst0 (minus x2 n0) v e1 e2)) (\lambda (e1:
+C).(drop (S n0) O (CHead c (Bind b) t) e1)))) (\lambda (H15: (drop n0 O c
+e2)).(or_introl (drop (S n0) O (CHead c (Bind b) t) e2) (ex2 C (\lambda (e1:
+C).(csubst0 (minus x2 n0) v e1 e2)) (\lambda (e1: C).(drop (S n0) O (CHead c
+(Bind b) t) e1))) (drop_drop (Bind b) n0 c e2 H15 t))) (\lambda (H15: (ex2 C
+(\lambda (e1: C).(csubst0 (minus x2 n0) v e1 e2)) (\lambda (e1: C).(drop n0 O
+c e1)))).(ex2_ind C (\lambda (e1: C).(csubst0 (minus x2 n0) v e1 e2))
+(\lambda (e1: C).(drop n0 O c e1)) (or (drop (S n0) O (CHead c (Bind b) t)
+e2) (ex2 C (\lambda (e1: C).(csubst0 (minus x2 n0) v e1 e2)) (\lambda (e1:
+C).(drop (S n0) O (CHead c (Bind b) t) e1)))) (\lambda (x: C).(\lambda (H16:
+(csubst0 (minus x2 n0) v x e2)).(\lambda (H17: (drop n0 O c x)).(or_intror
+(drop (S n0) O (CHead c (Bind b) t) e2) (ex2 C (\lambda (e1: C).(csubst0
+(minus x2 n0) v e1 e2)) (\lambda (e1: C).(drop (S n0) O (CHead c (Bind b) t)
+e1))) (ex_intro2 C (\lambda (e1: C).(csubst0 (minus x2 n0) v e1 e2)) (\lambda
+(e1: C).(drop (S n0) O (CHead c (Bind b) t) e1)) x H16 (drop_drop (Bind b) n0
+c x H17 t)))))) H15)) H14))))))) (\lambda (f: F).(\lambda (H11: ((\forall
+(c3: C).(\forall (v0: T).((csubst0 (s (Flat f) x2) v0 c c3) \to (\forall (e3:
+C).((drop (S n0) O c3 e3) \to (or (drop (S n0) O c e3) (ex2 C (\lambda (e1:
+C).(csubst0 (minus (s (Flat f) x2) (S n0)) v0 e1 e3)) (\lambda (e1: C).(drop
+(S n0) O c e1))))))))))).(\lambda (_: (lt (S n0) (s (Flat f) x2))).(\lambda
+(H13: (drop (r (Flat f) n0) O x1 e2)).(let H_x \def (H11 x1 v H7 e2 H13) in
+(let H14 \def H_x in (or_ind (drop (S n0) O c e2) (ex2 C (\lambda (e1:
+C).(csubst0 (minus x2 (S n0)) v e1 e2)) (\lambda (e1: C).(drop (S n0) O c
+e1))) (or (drop (S n0) O (CHead c (Flat f) t) e2) (ex2 C (\lambda (e1:
+C).(csubst0 (minus x2 (S n0)) v e1 e2)) (\lambda (e1: C).(drop (S n0) O
+(CHead c (Flat f) t) e1)))) (\lambda (H15: (drop (S n0) O c e2)).(or_introl
+(drop (S n0) O (CHead c (Flat f) t) e2) (ex2 C (\lambda (e1: C).(csubst0
+(minus x2 (S n0)) v e1 e2)) (\lambda (e1: C).(drop (S n0) O (CHead c (Flat f)
+t) e1))) (drop_drop (Flat f) n0 c e2 H15 t))) (\lambda (H15: (ex2 C (\lambda
+(e1: C).(csubst0 (minus x2 (S n0)) v e1 e2)) (\lambda (e1: C).(drop (S n0) O
+c e1)))).(ex2_ind C (\lambda (e1: C).(csubst0 (minus x2 (S n0)) v e1 e2))
+(\lambda (e1: C).(drop (S n0) O c e1)) (or (drop (S n0) O (CHead c (Flat f)
+t) e2) (ex2 C (\lambda (e1: C).(csubst0 (minus x2 (S n0)) v e1 e2)) (\lambda
+(e1: C).(drop (S n0) O (CHead c (Flat f) t) e1)))) (\lambda (x: C).(\lambda
+(H16: (csubst0 (minus x2 (S n0)) v x e2)).(\lambda (H17: (drop (S n0) O c
+x)).(or_intror (drop (S n0) O (CHead c (Flat f) t) e2) (ex2 C (\lambda (e1:
+C).(csubst0 (minus x2 (S n0)) v e1 e2)) (\lambda (e1: C).(drop (S n0) O
+(CHead c (Flat f) t) e1))) (ex_intro2 C (\lambda (e1: C).(csubst0 (minus x2
+(S n0)) v e1 e2)) (\lambda (e1: C).(drop (S n0) O (CHead c (Flat f) t) e1)) x
+H16 (drop_drop (Flat f) n0 c x H17 t)))))) H15)) H14))))))) k H9 H10
+(drop_gen_drop k x1 e2 x0 n0 H8)) i H4))))))))))) H3)) (csubst0_gen_head k c
+c2 t v i H1))))))))))) c1)))))) n).
+
projects / helm.git / blobdiff