DEFINITION pc3_gen_lift_abst()
TYPE =
∀c:C
.∀t:T
.∀t2:T
.∀u2:T
.∀h:nat
.∀d:nat
.pc3 c (lift h d t) (THead (Bind Abst) u2 t2)
→∀e:C
.drop h d c e
→(ex3_2
T
T
λu1:T.λt1:T.pr3 e t (THead (Bind Abst) u1 t1)
λu1:T.λ:T.pr3 c u2 (lift h d u1)
λ:T.λt1:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t2 (lift h (S d) t1)))
BODY =
assume c: C
assume t: T
assume t2: T
assume u2: T
assume h: nat
assume d: nat
suppose H: pc3 c (lift h d t) (THead (Bind Abst) u2 t2)
assume e: C
suppose H0: drop h d c e
(H1) consider H
consider H1
we proved pc3 c (lift h d t) (THead (Bind Abst) u2 t2)
that is equivalent to ex2 T λt0:T.pr3 c (lift h d t) t0 λt0:T.pr3 c (THead (Bind Abst) u2 t2) t0
we proceed by induction on the previous result to prove
ex3_2
T
T
λu1:T.λt1:T.pr3 e t (THead (Bind Abst) u1 t1)
λu1:T.λ:T.pr3 c u2 (lift h d u1)
λ:T.λt1:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t2 (lift h (S d) t1))
case ex_intro2 : x:T H2:pr3 c (lift h d t) x H3:pr3 c (THead (Bind Abst) u2 t2) x ⇒
the thesis becomes
ex3_2
T
T
λu1:T.λt1:T.pr3 e t (THead (Bind Abst) u1 t1)
λu1:T.λ:T.pr3 c u2 (lift h d u1)
λ:T.λt1:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t2 (lift h (S d) t1))
(H4)
by (pr3_gen_lift . . . . . H2 . H0)
ex2 T λt2:T.eq T x (lift h d t2) λt2:T.pr3 e t t2
end of H4
we proceed by induction on H4 to prove
ex3_2
T
T
λu1:T.λt1:T.pr3 e t (THead (Bind Abst) u1 t1)
λu1:T.λ:T.pr3 c u2 (lift h d u1)
λ:T.λt1:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t2 (lift h (S d) t1))
case ex_intro2 : x0:T H5:eq T x (lift h d x0) H6:pr3 e t x0 ⇒
the thesis becomes
ex3_2
T
T
λu1:T.λt1:T.pr3 e t (THead (Bind Abst) u1 t1)
λu1:T.λ:T.pr3 c u2 (lift h d u1)
λ:T.λt1:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t2 (lift h (S d) t1))
(H7)
by (pr3_gen_abst . . . . H3)
ex3_2
T
T
λu2:T.λt2:T.eq T x (THead (Bind Abst) u2 t2)
λu2:T.λ:T.pr3 c u2 u2
λ:T.λt2:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t2 t2)
end of H7
we proceed by induction on H7 to prove
ex3_2
T
T
λu1:T.λt1:T.pr3 e t (THead (Bind Abst) u1 t1)
λu1:T.λ:T.pr3 c u2 (lift h d u1)
λ:T.λt1:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t2 (lift h (S d) t1))
case ex3_2_intro : x1:T x2:T H8:eq T x (THead (Bind Abst) x1 x2) H9:pr3 c u2 x1 H10:∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t2 x2) ⇒
the thesis becomes
ex3_2
T
T
λu1:T.λt1:T.pr3 e t (THead (Bind Abst) u1 t1)
λu1:T.λ:T.pr3 c u2 (lift h d u1)
λ:T.λt1:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t2 (lift h (S d) t1))
(H11)
we proceed by induction on H8 to prove eq T (THead (Bind Abst) x1 x2) (lift h d x0)
case refl_equal : ⇒
the thesis becomes the hypothesis H5
eq T (THead (Bind Abst) x1 x2) (lift h d x0)
end of H11
by (lift_gen_bind . . . . . . H11)
we proved
ex3_2
T
T
λy:T.λz:T.eq T x0 (THead (Bind Abst) y z)
λy:T.λ:T.eq T x1 (lift h d y)
λ:T.λz:T.eq T x2 (lift h (S d) z)
we proceed by induction on the previous result to prove
ex3_2
T
T
λu1:T.λt1:T.pr3 e t (THead (Bind Abst) u1 t1)
λu1:T.λ:T.pr3 c u2 (lift h d u1)
λ:T.λt1:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t2 (lift h (S d) t1))
case ex3_2_intro : x3:T x4:T H12:eq T x0 (THead (Bind Abst) x3 x4) H13:eq T x1 (lift h d x3) H14:eq T x2 (lift h (S d) x4) ⇒
the thesis becomes
ex3_2
T
T
λu1:T.λt1:T.pr3 e t (THead (Bind Abst) u1 t1)
λu1:T.λ:T.pr3 c u2 (lift h d u1)
λ:T.λt1:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t2 (lift h (S d) t1))
(H15)
we proceed by induction on H14 to prove ∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t2 (lift h (S d) x4))
case refl_equal : ⇒
the thesis becomes the hypothesis H10
∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t2 (lift h (S d) x4))
end of H15
(H16)
we proceed by induction on H13 to prove pr3 c u2 (lift h d x3)
case refl_equal : ⇒
the thesis becomes the hypothesis H9
pr3 c u2 (lift h d x3)
end of H16
(H17)
we proceed by induction on H12 to prove pr3 e t (THead (Bind Abst) x3 x4)
case refl_equal : ⇒
the thesis becomes the hypothesis H6
pr3 e t (THead (Bind Abst) x3 x4)
end of H17
by (ex3_2_intro . . . . . . . H17 H16 H15)
ex3_2
T
T
λu1:T.λt1:T.pr3 e t (THead (Bind Abst) u1 t1)
λu1:T.λ:T.pr3 c u2 (lift h d u1)
λ:T.λt1:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t2 (lift h (S d) t1))
ex3_2
T
T
λu1:T.λt1:T.pr3 e t (THead (Bind Abst) u1 t1)
λu1:T.λ:T.pr3 c u2 (lift h d u1)
λ:T.λt1:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t2 (lift h (S d) t1))
ex3_2
T
T
λu1:T.λt1:T.pr3 e t (THead (Bind Abst) u1 t1)
λu1:T.λ:T.pr3 c u2 (lift h d u1)
λ:T.λt1:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t2 (lift h (S d) t1))
ex3_2
T
T
λu1:T.λt1:T.pr3 e t (THead (Bind Abst) u1 t1)
λu1:T.λ:T.pr3 c u2 (lift h d u1)
λ:T.λt1:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t2 (lift h (S d) t1))
we proved
ex3_2
T
T
λu1:T.λt1:T.pr3 e t (THead (Bind Abst) u1 t1)
λu1:T.λ:T.pr3 c u2 (lift h d u1)
λ:T.λt1:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t2 (lift h (S d) t1))
we proved
∀c:C
.∀t:T
.∀t2:T
.∀u2:T
.∀h:nat
.∀d:nat
.pc3 c (lift h d t) (THead (Bind Abst) u2 t2)
→∀e:C
.drop h d c e
→(ex3_2
T
T
λu1:T.λt1:T.pr3 e t (THead (Bind Abst) u1 t1)
λu1:T.λ:T.pr3 c u2 (lift h d u1)
λ:T.λt1:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t2 (lift h (S d) t1)))