DEFINITION ty3_gen_appl_nf2()
TYPE =
∀g:G
.∀c:C
.∀w:T
.∀v:T
.∀x:T
.ty3 g c (THead (Flat Appl) w v) x
→(ex4_2
T
T
λu:T.λt:T.pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x
λu:T.λt:T.ty3 g c v (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c w u
λu:T.λt:T.nf2 c (THead (Bind Abst) u t))
BODY =
assume g: G
assume c: C
assume w: T
assume v: T
assume x: T
suppose H: ty3 g c (THead (Flat Appl) w v) x
by (ty3_gen_appl . . . . . H)
we proved
ex3_2
T
T
λu:T.λt:T.pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x
λu:T.λt:T.ty3 g c v (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c w u
we proceed by induction on the previous result to prove
ex4_2
T
T
λu:T.λt:T.pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x
λu:T.λt:T.ty3 g c v (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c w u
λu:T.λt:T.nf2 c (THead (Bind Abst) u t)
case ex3_2_intro : x0:T x1:T H0:pc3 c (THead (Flat Appl) w (THead (Bind Abst) x0 x1)) x H1:ty3 g c v (THead (Bind Abst) x0 x1) H2:ty3 g c w x0 ⇒
the thesis becomes
ex4_2
T
T
λu:T.λt:T.pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x
λu:T.λt:T.ty3 g c v (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c w u
λu:T.λt:T.nf2 c (THead (Bind Abst) u t)
(H_x)
by (ty3_correct . . . . H1)
ex T λt:T.ty3 g c (THead (Bind Abst) x0 x1) t
end of H_x
(H3) consider H_x
we proceed by induction on H3 to prove
ex4_2
T
T
λu:T.λt:T.pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x
λu:T.λt:T.ty3 g c v (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c w u
λu:T.λt:T.nf2 c (THead (Bind Abst) u t)
case ex_intro : x2:T H4:ty3 g c (THead (Bind Abst) x0 x1) x2 ⇒
the thesis becomes
ex4_2
T
T
λu:T.λt:T.pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x
λu:T.λt:T.ty3 g c v (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c w u
λu:T.λt:T.nf2 c (THead (Bind Abst) u t)
(H_x0)
by (ty3_correct . . . . H2)
ex T λt:T.ty3 g c x0 t
end of H_x0
(H5) consider H_x0
we proceed by induction on H5 to prove
ex4_2
T
T
λu:T.λt:T.pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x
λu:T.λt:T.ty3 g c v (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c w u
λu:T.λt:T.nf2 c (THead (Bind Abst) u t)
case ex_intro : x3:T H6:ty3 g c x0 x3 ⇒
the thesis becomes
ex4_2
T
T
λu:T.λt:T.pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x
λu:T.λt:T.ty3 g c v (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c w u
λu:T.λt:T.nf2 c (THead (Bind Abst) u t)
(H7)
by (ty3_sn3 . . . . H4)
sn3 c (THead (Bind Abst) x0 x1)
end of H7
(H_x1)
by (nf2_sn3 . . H7)
ex2 T λu:T.pr3 c (THead (Bind Abst) x0 x1) u λu:T.nf2 c u
end of H_x1
(H8) consider H_x1
we proceed by induction on H8 to prove
ex4_2
T
T
λu:T.λt:T.pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x
λu:T.λt:T.ty3 g c v (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c w u
λu:T.λt:T.nf2 c (THead (Bind Abst) u t)
case ex_intro2 : x4:T H9:pr3 c (THead (Bind Abst) x0 x1) x4 H10:nf2 c x4 ⇒
the thesis becomes
ex4_2
T
T
λu:T.λt:T.pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x
λu:T.λt:T.ty3 g c v (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c w u
λu:T.λt:T.nf2 c (THead (Bind Abst) u t)
(H11)
by (pr3_gen_abst . . . . H9)
ex3_2
T
T
λu2:T.λt2:T.eq T x4 (THead (Bind Abst) u2 t2)
λu2:T.λ:T.pr3 c x0 u2
λ:T.λt2:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) x1 t2)
end of H11
we proceed by induction on H11 to prove
ex4_2
T
T
λu:T.λt:T.pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x
λu:T.λt:T.ty3 g c v (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c w u
λu:T.λt:T.nf2 c (THead (Bind Abst) u t)
case ex3_2_intro : x5:T x6:T H12:eq T x4 (THead (Bind Abst) x5 x6) H13:pr3 c x0 x5 H14:∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) x1 x6) ⇒
the thesis becomes
ex4_2
T
T
λu:T.λt:T.pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x
λu:T.λt:T.ty3 g c v (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c w u
λu:T.λt:T.nf2 c (THead (Bind Abst) u t)
(H15)
we proceed by induction on H12 to prove nf2 c (THead (Bind Abst) x5 x6)
case refl_equal : ⇒
the thesis becomes the hypothesis H10
nf2 c (THead (Bind Abst) x5 x6)
end of H15
(H16)
by (H14 . .)
we proved pr3 (CHead c (Bind Abst) x5) x1 x6
by (pr3_head_12 . . . H13 . . . previous)
pr3 c (THead (Bind Abst) x0 x1) (THead (Bind Abst) x5 x6)
end of H16
(h1)
by (pr3_thin_dx . . . H16 . .)
we proved
pr3
c
THead (Flat Appl) w (THead (Bind Abst) x0 x1)
THead (Flat Appl) w (THead (Bind Abst) x5 x6)
by (pc3_pr3_conf . . . H0 . previous)
pc3 c (THead (Flat Appl) w (THead (Bind Abst) x5 x6)) x
end of h1
(h2)
(h1)
by (ty3_sred_pr3 . . . H16 . . H4)
ty3 g c (THead (Bind Abst) x5 x6) x2
end of h1
(h2)
by (pc3_pr3_r . . . H16)
pc3 c (THead (Bind Abst) x0 x1) (THead (Bind Abst) x5 x6)
end of h2
by (ty3_conv . . . . h1 . . H1 h2)
ty3 g c v (THead (Bind Abst) x5 x6)
end of h2
(h3)
(h1) by (ty3_sred_pr3 . . . H13 . . H6) we proved ty3 g c x5 x3
(h2)
by (pc3_pr3_r . . . H13)
pc3 c x0 x5
end of h2
by (ty3_conv . . . . h1 . . H2 h2)
ty3 g c w x5
end of h3
by (ex4_2_intro . . . . . . . . h1 h2 h3 H15)
ex4_2
T
T
λu:T.λt:T.pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x
λu:T.λt:T.ty3 g c v (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c w u
λu:T.λt:T.nf2 c (THead (Bind Abst) u t)
ex4_2
T
T
λu:T.λt:T.pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x
λu:T.λt:T.ty3 g c v (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c w u
λu:T.λt:T.nf2 c (THead (Bind Abst) u t)
ex4_2
T
T
λu:T.λt:T.pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x
λu:T.λt:T.ty3 g c v (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c w u
λu:T.λt:T.nf2 c (THead (Bind Abst) u t)
ex4_2
T
T
λu:T.λt:T.pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x
λu:T.λt:T.ty3 g c v (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c w u
λu:T.λt:T.nf2 c (THead (Bind Abst) u t)
ex4_2
T
T
λu:T.λt:T.pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x
λu:T.λt:T.ty3 g c v (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c w u
λu:T.λt:T.nf2 c (THead (Bind Abst) u t)
we proved
ex4_2
T
T
λu:T.λt:T.pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x
λu:T.λt:T.ty3 g c v (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c w u
λu:T.λt:T.nf2 c (THead (Bind Abst) u t)
we proved
∀g:G
.∀c:C
.∀w:T
.∀v:T
.∀x:T
.ty3 g c (THead (Flat Appl) w v) x
→(ex4_2
T
T
λu:T.λt:T.pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x
λu:T.λt:T.ty3 g c v (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c w u
λu:T.λt:T.nf2 c (THead (Bind Abst) u t))