DEFINITION wcpr0_drop_back()
TYPE =
∀c1:C
.∀c2:C
.wcpr0 c2 c1
→∀h:nat
.∀e1:C
.∀u1:T
.∀k:K
.drop h O c1 (CHead e1 k u1)
→ex3_2 C T λe2:C.λu2:T.drop h O c2 (CHead e2 k u2) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu2:T.pr0 u2 u1
BODY =
assume c1: C
assume c2: C
suppose H: wcpr0 c2 c1
we proceed by induction on H to prove
∀h:nat
.∀e1:C
.∀u1:T
.∀k:K
.drop h O c1 (CHead e1 k u1)
→ex3_2 C T λe2:C.λu2:T.drop h O c2 (CHead e2 k u2) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu2:T.pr0 u2 u1
case wcpr0_refl : c:C ⇒
the thesis becomes
∀h:nat
.∀e1:C
.∀u1:T
.∀k:K
.∀H0:(drop h O c (CHead e1 k u1)).(ex3_2 C T λe2:C.λu2:T.drop h O c (CHead e2 k u2) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu2:T.pr0 u2 u1)
assume h: nat
assume e1: C
assume u1: T
assume k: K
suppose H0: drop h O c (CHead e1 k u1)
(h1) by (wcpr0_refl .) we proved wcpr0 e1 e1
(h2) by (pr0_refl .) we proved pr0 u1 u1
by (ex3_2_intro . . . . . . . H0 h1 h2)
we proved ex3_2 C T λe2:C.λu2:T.drop h O c (CHead e2 k u2) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu2:T.pr0 u2 u1
∀h:nat
.∀e1:C
.∀u1:T
.∀k:K
.∀H0:(drop h O c (CHead e1 k u1)).(ex3_2 C T λe2:C.λu2:T.drop h O c (CHead e2 k u2) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu2:T.pr0 u2 u1)
case wcpr0_comp : c3:C c4:C H0:wcpr0 c3 c4 u1:T u2:T H2:pr0 u1 u2 k:K ⇒
the thesis becomes
∀h:nat
.∀e1:C
.∀u3:T
.∀k0:K
.drop h O (CHead c4 k u2) (CHead e1 k0 u3)
→ex3_2 C T λe2:C.λu4:T.drop h O (CHead c3 k u1) (CHead e2 k0 u4) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu4:T.pr0 u4 u3
(H1) by induction hypothesis we know
∀h:nat
.∀e1:C
.∀u1:T
.∀k:K
.drop h O c4 (CHead e1 k u1)
→ex3_2 C T λe2:C.λu2:T.drop h O c3 (CHead e2 k u2) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu2:T.pr0 u2 u1
assume h: nat
we proceed by induction on h to prove
∀e1:C
.∀u3:T
.∀k0:K
.drop h O (CHead c4 k u2) (CHead e1 k0 u3)
→ex3_2 C T λe2:C.λu4:T.drop h O (CHead c3 k u1) (CHead e2 k0 u4) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu4:T.pr0 u4 u3
case O : ⇒
the thesis becomes
∀e1:C
.∀u0:T
.∀k0:K
.drop O O (CHead c4 k u2) (CHead e1 k0 u0)
→ex3_2 C T λe2:C.λu3:T.drop O O (CHead c3 k u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
assume e1: C
assume u0: T
assume k0: K
suppose H3: drop O O (CHead c4 k u2) (CHead e1 k0 u0)
(H4)
by (drop_gen_refl . . H3)
we proved eq C (CHead c4 k u2) (CHead e1 k0 u0)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead c4 k u2 OF CSort ⇒c4 | CHead c ⇒c
<λ:C.C> CASE CHead e1 k0 u0 OF CSort ⇒c4 | CHead c ⇒c
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒c4 | CHead c ⇒c (CHead c4 k u2)
λe:C.<λ:C.C> CASE e OF CSort ⇒c4 | CHead c ⇒c (CHead e1 k0 u0)
end of H4
(h1)
(H5)
by (drop_gen_refl . . H3)
we proved eq C (CHead c4 k u2) (CHead e1 k0 u0)
by (f_equal . . . . . previous)
we proved
eq
K
<λ:C.K> CASE CHead c4 k u2 OF CSort ⇒k | CHead k1 ⇒k1
<λ:C.K> CASE CHead e1 k0 u0 OF CSort ⇒k | CHead k1 ⇒k1
eq
K
λe:C.<λ:C.K> CASE e OF CSort ⇒k | CHead k1 ⇒k1 (CHead c4 k u2)
λe:C.<λ:C.K> CASE e OF CSort ⇒k | CHead k1 ⇒k1 (CHead e1 k0 u0)
end of H5
(h1)
(H6)
by (drop_gen_refl . . H3)
we proved eq C (CHead c4 k u2) (CHead e1 k0 u0)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead c4 k u2 OF CSort ⇒u2 | CHead t⇒t
<λ:C.T> CASE CHead e1 k0 u0 OF CSort ⇒u2 | CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u2 | CHead t⇒t (CHead c4 k u2)
λe:C.<λ:C.T> CASE e OF CSort ⇒u2 | CHead t⇒t (CHead e1 k0 u0)
end of H6
suppose H7: eq K k k0
suppose H8: eq C c4 e1
we proceed by induction on H7 to prove ex3_2 C T λe2:C.λu3:T.drop O O (CHead c3 k u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
case refl_equal : ⇒
the thesis becomes ex3_2 C T λe2:C.λu3:T.drop O O (CHead c3 k u1) (CHead e2 k u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
consider H6
we proved
eq
T
<λ:C.T> CASE CHead c4 k u2 OF CSort ⇒u2 | CHead t⇒t
<λ:C.T> CASE CHead e1 k0 u0 OF CSort ⇒u2 | CHead t⇒t
that is equivalent to eq T u2 u0
we proceed by induction on the previous result to prove ex3_2 C T λe2:C.λu3:T.drop O O (CHead c3 k u1) (CHead e2 k u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
case refl_equal : ⇒
the thesis becomes ex3_2 C T λe2:C.λu3:T.drop O O (CHead c3 k u1) (CHead e2 k u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u2
we proceed by induction on H8 to prove ex3_2 C T λe2:C.λu3:T.drop O O (CHead c3 k u1) (CHead e2 k u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u2
case refl_equal : ⇒
the thesis becomes ex3_2 C T λe2:C.λu3:T.drop O O (CHead c3 k u1) (CHead e2 k u3) λe2:C.λ:T.wcpr0 e2 c4 λ:C.λu3:T.pr0 u3 u2
by (drop_refl .)
we proved drop O O (CHead c3 k u1) (CHead c3 k u1)
by (ex3_2_intro . . . . . . . previous H0 H2)
ex3_2 C T λe2:C.λu3:T.drop O O (CHead c3 k u1) (CHead e2 k u3) λe2:C.λ:T.wcpr0 e2 c4 λ:C.λu3:T.pr0 u3 u2
ex3_2 C T λe2:C.λu3:T.drop O O (CHead c3 k u1) (CHead e2 k u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u2
ex3_2 C T λe2:C.λu3:T.drop O O (CHead c3 k u1) (CHead e2 k u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
we proved ex3_2 C T λe2:C.λu3:T.drop O O (CHead c3 k u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
eq K k k0
→(eq C c4 e1)→(ex3_2 C T λe2:C.λu3:T.drop O O (CHead c3 k u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0)
end of h1
(h2)
consider H5
we proved
eq
K
<λ:C.K> CASE CHead c4 k u2 OF CSort ⇒k | CHead k1 ⇒k1
<λ:C.K> CASE CHead e1 k0 u0 OF CSort ⇒k | CHead k1 ⇒k1
eq K k k0
end of h2
by (h1 h2)
(eq C c4 e1)→(ex3_2 C T λe2:C.λu3:T.drop O O (CHead c3 k u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0)
end of h1
(h2)
consider H4
we proved
eq
C
<λ:C.C> CASE CHead c4 k u2 OF CSort ⇒c4 | CHead c ⇒c
<λ:C.C> CASE CHead e1 k0 u0 OF CSort ⇒c4 | CHead c ⇒c
eq C c4 e1
end of h2
by (h1 h2)
we proved ex3_2 C T λe2:C.λu3:T.drop O O (CHead c3 k u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
∀e1:C
.∀u0:T
.∀k0:K
.drop O O (CHead c4 k u2) (CHead e1 k0 u0)
→ex3_2 C T λe2:C.λu3:T.drop O O (CHead c3 k u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
case S ⇒
we need to prove
∀n:nat
.∀e1:C
.∀u3:T
.∀k1:K
.drop n O (CHead c4 k u2) (CHead e1 k1 u3)
→ex3_2 C T λe2:C.λu4:T.drop n O (CHead c3 k u1) (CHead e2 k1 u4) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu4:T.pr0 u4 u3
→∀e1:C
.∀u3:T
.∀k1:K
.drop (S n) O (CHead c4 k u2) (CHead e1 k1 u3)
→ex3_2 C T λe2:C.λu4:T.drop (S n) O (CHead c3 k u1) (CHead e2 k1 u4) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu4:T.pr0 u4 u3
we proceed by induction on k to prove
∀n:nat
.∀e1:C
.∀u3:T
.∀k1:K
.drop n O (CHead c4 k u2) (CHead e1 k1 u3)
→ex3_2 C T λe2:C.λu4:T.drop n O (CHead c3 k u1) (CHead e2 k1 u4) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu4:T.pr0 u4 u3
→∀e1:C
.∀u3:T
.∀k1:K
.drop (S n) O (CHead c4 k u2) (CHead e1 k1 u3)
→ex3_2 C T λe2:C.λu4:T.drop (S n) O (CHead c3 k u1) (CHead e2 k1 u4) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu4:T.pr0 u4 u3
case Bind : b:B ⇒
the thesis becomes
∀n:nat
.∀e1:C
.∀u3:T
.∀k0:K
.drop n O (CHead c4 (Bind b) u2) (CHead e1 k0 u3)
→ex3_2 C T λe2:C.λu4:T.drop n O (CHead c3 (Bind b) u1) (CHead e2 k0 u4) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu4:T.pr0 u4 u3
→∀e1:C
.∀u0:T
.∀k0:K
.∀H4:drop (S n) O (CHead c4 (Bind b) u2) (CHead e1 k0 u0)
.ex3_2 C T λe2:C.λu3:T.drop (S n) O (CHead c3 (Bind b) u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
assume n: nat
suppose :
∀e1:C
.∀u3:T
.∀k0:K
.drop n O (CHead c4 (Bind b) u2) (CHead e1 k0 u3)
→ex3_2 C T λe2:C.λu4:T.drop n O (CHead c3 (Bind b) u1) (CHead e2 k0 u4) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu4:T.pr0 u4 u3
assume e1: C
assume u0: T
assume k0: K
suppose H4: drop (S n) O (CHead c4 (Bind b) u2) (CHead e1 k0 u0)
(H5)
by (drop_gen_drop . . . . . H4)
we proved drop (r (Bind b) n) O c4 (CHead e1 k0 u0)
that is equivalent to drop n O c4 (CHead e1 k0 u0)
by (H1 . . . . previous)
ex3_2 C T λe2:C.λu2:T.drop n O c3 (CHead e2 k0 u2) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu2:T.pr0 u2 u0
end of H5
we proceed by induction on H5 to prove ex3_2 C T λe2:C.λu3:T.drop (S n) O (CHead c3 (Bind b) u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
case ex3_2_intro : x0:C x1:T H6:drop n O c3 (CHead x0 k0 x1) H7:wcpr0 x0 e1 H8:pr0 x1 u0 ⇒
the thesis becomes ex3_2 C T λe2:C.λu3:T.drop (S n) O (CHead c3 (Bind b) u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
consider H6
we proved drop n O c3 (CHead x0 k0 x1)
that is equivalent to drop (r (Bind b) n) O c3 (CHead x0 k0 x1)
by (drop_drop . . . . previous .)
we proved drop (S n) O (CHead c3 (Bind b) u1) (CHead x0 k0 x1)
by (ex3_2_intro . . . . . . . previous H7 H8)
ex3_2 C T λe2:C.λu3:T.drop (S n) O (CHead c3 (Bind b) u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
we proved ex3_2 C T λe2:C.λu3:T.drop (S n) O (CHead c3 (Bind b) u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
∀n:nat
.∀e1:C
.∀u3:T
.∀k0:K
.drop n O (CHead c4 (Bind b) u2) (CHead e1 k0 u3)
→ex3_2 C T λe2:C.λu4:T.drop n O (CHead c3 (Bind b) u1) (CHead e2 k0 u4) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu4:T.pr0 u4 u3
→∀e1:C
.∀u0:T
.∀k0:K
.∀H4:drop (S n) O (CHead c4 (Bind b) u2) (CHead e1 k0 u0)
.ex3_2 C T λe2:C.λu3:T.drop (S n) O (CHead c3 (Bind b) u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
case Flat : f:F ⇒
the thesis becomes
∀n:nat
.∀e1:C
.∀u3:T
.∀k0:K
.drop n O (CHead c4 (Flat f) u2) (CHead e1 k0 u3)
→ex3_2 C T λe2:C.λu4:T.drop n O (CHead c3 (Flat f) u1) (CHead e2 k0 u4) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu4:T.pr0 u4 u3
→∀e1:C
.∀u0:T
.∀k0:K
.∀H4:drop (S n) O (CHead c4 (Flat f) u2) (CHead e1 k0 u0)
.ex3_2 C T λe2:C.λu3:T.drop (S n) O (CHead c3 (Flat f) u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
assume n: nat
suppose :
∀e1:C
.∀u3:T
.∀k0:K
.drop n O (CHead c4 (Flat f) u2) (CHead e1 k0 u3)
→ex3_2 C T λe2:C.λu4:T.drop n O (CHead c3 (Flat f) u1) (CHead e2 k0 u4) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu4:T.pr0 u4 u3
assume e1: C
assume u0: T
assume k0: K
suppose H4: drop (S n) O (CHead c4 (Flat f) u2) (CHead e1 k0 u0)
(H5)
by (drop_gen_drop . . . . . H4)
we proved drop (r (Flat f) n) O c4 (CHead e1 k0 u0)
that is equivalent to drop (S n) O c4 (CHead e1 k0 u0)
by (H1 . . . . previous)
ex3_2 C T λe2:C.λu2:T.drop (S n) O c3 (CHead e2 k0 u2) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu2:T.pr0 u2 u0
end of H5
we proceed by induction on H5 to prove ex3_2 C T λe2:C.λu3:T.drop (S n) O (CHead c3 (Flat f) u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
case ex3_2_intro : x0:C x1:T H6:drop (S n) O c3 (CHead x0 k0 x1) H7:wcpr0 x0 e1 H8:pr0 x1 u0 ⇒
the thesis becomes ex3_2 C T λe2:C.λu3:T.drop (S n) O (CHead c3 (Flat f) u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
consider H6
we proved drop (S n) O c3 (CHead x0 k0 x1)
that is equivalent to drop (r (Flat f) n) O c3 (CHead x0 k0 x1)
by (drop_drop . . . . previous .)
we proved drop (S n) O (CHead c3 (Flat f) u1) (CHead x0 k0 x1)
by (ex3_2_intro . . . . . . . previous H7 H8)
ex3_2 C T λe2:C.λu3:T.drop (S n) O (CHead c3 (Flat f) u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
we proved ex3_2 C T λe2:C.λu3:T.drop (S n) O (CHead c3 (Flat f) u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
∀n:nat
.∀e1:C
.∀u3:T
.∀k0:K
.drop n O (CHead c4 (Flat f) u2) (CHead e1 k0 u3)
→ex3_2 C T λe2:C.λu4:T.drop n O (CHead c3 (Flat f) u1) (CHead e2 k0 u4) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu4:T.pr0 u4 u3
→∀e1:C
.∀u0:T
.∀k0:K
.∀H4:drop (S n) O (CHead c4 (Flat f) u2) (CHead e1 k0 u0)
.ex3_2 C T λe2:C.λu3:T.drop (S n) O (CHead c3 (Flat f) u1) (CHead e2 k0 u3) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu3:T.pr0 u3 u0
∀n:nat
.∀e1:C
.∀u3:T
.∀k1:K
.drop n O (CHead c4 k u2) (CHead e1 k1 u3)
→ex3_2 C T λe2:C.λu4:T.drop n O (CHead c3 k u1) (CHead e2 k1 u4) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu4:T.pr0 u4 u3
→∀e1:C
.∀u3:T
.∀k1:K
.drop (S n) O (CHead c4 k u2) (CHead e1 k1 u3)
→ex3_2 C T λe2:C.λu4:T.drop (S n) O (CHead c3 k u1) (CHead e2 k1 u4) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu4:T.pr0 u4 u3
we proved
∀e1:C
.∀u3:T
.∀k0:K
.drop h O (CHead c4 k u2) (CHead e1 k0 u3)
→ex3_2 C T λe2:C.λu4:T.drop h O (CHead c3 k u1) (CHead e2 k0 u4) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu4:T.pr0 u4 u3
∀h:nat
.∀e1:C
.∀u3:T
.∀k0:K
.drop h O (CHead c4 k u2) (CHead e1 k0 u3)
→ex3_2 C T λe2:C.λu4:T.drop h O (CHead c3 k u1) (CHead e2 k0 u4) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu4:T.pr0 u4 u3
we proved
∀h:nat
.∀e1:C
.∀u1:T
.∀k:K
.drop h O c1 (CHead e1 k u1)
→ex3_2 C T λe2:C.λu2:T.drop h O c2 (CHead e2 k u2) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu2:T.pr0 u2 u1
we proved
∀c1:C
.∀c2:C
.wcpr0 c2 c1
→∀h:nat
.∀e1:C
.∀u1:T
.∀k:K
.drop h O c1 (CHead e1 k u1)
→ex3_2 C T λe2:C.λu2:T.drop h O c2 (CHead e2 k u2) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu2:T.pr0 u2 u1