DEFINITION ty3_inv_appls_lref_nf2()
TYPE =
∀g:G
.∀c:C
.∀vs:TList
.∀u1:T
.∀i:nat
.ty3 g c (THeads (Flat Appl) vs (TLRef i)) u1
→(nf2 c (TLRef i)
→(nf2 c u1
→(ex2
T
λu:T.nf2 c (lift (S i) O u)
λu:T.pc3 c (THeads (Flat Appl) vs (lift (S i) O u)) u1)))
BODY =
assume g: G
assume c: C
assume vs: TList
we proceed by induction on vs to prove
∀u1:T
.∀i:nat
.ty3 g c (THeads (Flat Appl) vs (TLRef i)) u1
→(nf2 c (TLRef i)
→(nf2 c u1
→(ex2
T
λu:T.nf2 c (lift (S i) O u)
λu:T.pc3 c (THeads (Flat Appl) vs (lift (S i) O u)) u1)))
case TNil : ⇒
the thesis becomes
∀u1:T
.∀i:nat
.ty3 g c (THeads (Flat Appl) TNil (TLRef i)) u1
→(nf2 c (TLRef i)
→(nf2 c u1
→(ex2
T
λu:T.nf2 c (lift (S i) O u)
λu:T.pc3 c (THeads (Flat Appl) TNil (lift (S i) O u)) u1)))
assume u1: T
assume i: nat
we must prove
ty3 g c (THeads (Flat Appl) TNil (TLRef i)) u1
→(nf2 c (TLRef i)
→(nf2 c u1
→(ex2
T
λu:T.nf2 c (lift (S i) O u)
λu:T.pc3 c (THeads (Flat Appl) TNil (lift (S i) O u)) u1)))
or equivalently
ty3 g c (TLRef i) u1
→(nf2 c (TLRef i)
→(nf2 c u1
→(ex2
T
λu:T.nf2 c (lift (S i) O u)
λu:T.pc3 c (THeads (Flat Appl) TNil (lift (S i) O u)) u1)))
suppose H: ty3 g c (TLRef i) u1
suppose H0: nf2 c (TLRef i)
suppose H1: nf2 c u1
(H_x)
by (ty3_inv_lref_nf2 . . . . H H0 H1)
ex T λu0:T.eq T u1 (lift (S i) O u0)
end of H_x
(H2) consider H_x
we proceed by induction on H2 to prove ex2 T λu:T.nf2 c (lift (S i) O u) λu:T.pc3 c (lift (S i) O u) u1
case ex_intro : x:T H3:eq T u1 (lift (S i) O x) ⇒
the thesis becomes ex2 T λu:T.nf2 c (lift (S i) O u) λu:T.pc3 c (lift (S i) O u) u1
(H4)
we proceed by induction on H3 to prove nf2 c (lift (S i) O x)
case refl_equal : ⇒
the thesis becomes the hypothesis H1
nf2 c (lift (S i) O x)
end of H4
by (pc3_refl . .)
we proved pc3 c (lift (S i) O x) (lift (S i) O x)
by (ex_intro2 . . . . H4 previous)
we proved
ex2
T
λu:T.nf2 c (lift (S i) O u)
λu:T.pc3 c (lift (S i) O u) (lift (S i) O x)
by (eq_ind_r . . . previous . H3)
ex2 T λu:T.nf2 c (lift (S i) O u) λu:T.pc3 c (lift (S i) O u) u1
we proved ex2 T λu:T.nf2 c (lift (S i) O u) λu:T.pc3 c (lift (S i) O u) u1
that is equivalent to
ex2
T
λu:T.nf2 c (lift (S i) O u)
λu:T.pc3 c (THeads (Flat Appl) TNil (lift (S i) O u)) u1
we proved
ty3 g c (TLRef i) u1
→(nf2 c (TLRef i)
→(nf2 c u1
→(ex2
T
λu:T.nf2 c (lift (S i) O u)
λu:T.pc3 c (THeads (Flat Appl) TNil (lift (S i) O u)) u1)))
that is equivalent to
ty3 g c (THeads (Flat Appl) TNil (TLRef i)) u1
→(nf2 c (TLRef i)
→(nf2 c u1
→(ex2
T
λu:T.nf2 c (lift (S i) O u)
λu:T.pc3 c (THeads (Flat Appl) TNil (lift (S i) O u)) u1)))
∀u1:T
.∀i:nat
.ty3 g c (THeads (Flat Appl) TNil (TLRef i)) u1
→(nf2 c (TLRef i)
→(nf2 c u1
→(ex2
T
λu:T.nf2 c (lift (S i) O u)
λu:T.pc3 c (THeads (Flat Appl) TNil (lift (S i) O u)) u1)))
case TCons : t:T t0:TList ⇒
the thesis becomes
∀u1:T
.∀i:nat
.ty3 g c (THeads (Flat Appl) (TCons t t0) (TLRef i)) u1
→(nf2 c (TLRef i)
→(nf2 c u1
→(ex2
T
λu:T.nf2 c (lift (S i) O u)
λu:T.pc3 c (THeads (Flat Appl) (TCons t t0) (lift (S i) O u)) u1)))
(H) by induction hypothesis we know
∀u1:T
.∀i:nat
.ty3 g c (THeads (Flat Appl) t0 (TLRef i)) u1
→(nf2 c (TLRef i)
→(nf2 c u1
→(ex2
T
λu:T.nf2 c (lift (S i) O u)
λu:T.pc3 c (THeads (Flat Appl) t0 (lift (S i) O u)) u1)))
assume u1: T
assume i: nat
we must prove
ty3 g c (THeads (Flat Appl) (TCons t t0) (TLRef i)) u1
→(nf2 c (TLRef i)
→(nf2 c u1
→(ex2
T
λu:T.nf2 c (lift (S i) O u)
λu:T.pc3 c (THeads (Flat Appl) (TCons t t0) (lift (S i) O u)) u1)))
or equivalently
ty3 g c (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) u1
→(nf2 c (TLRef i)
→(nf2 c u1
→(ex2
T
λu:T.nf2 c (lift (S i) O u)
λu:T.pc3 c (THeads (Flat Appl) (TCons t t0) (lift (S i) O u)) u1)))
suppose H0: ty3 g c (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) u1
suppose H1: nf2 c (TLRef i)
suppose : nf2 c u1
(H_x)
by (ty3_gen_appl_nf2 . . . . . H0)
ex4_2
T
T
λu:T.λt:T.pc3 c (THead (Flat Appl) t (THead (Bind Abst) u t)) u1
λu:T
.λt:T
.ty3 g c (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind Abst) u t)
λu:T.λ:T.ty3 g c t u
λu:T.λt:T.nf2 c (THead (Bind Abst) u t)
end of H_x
(H3) consider H_x
we proceed by induction on H3 to prove
ex2
T
λu:T.nf2 c (lift (S i) O u)
λu:T
.pc3
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O u))
u1
case ex4_2_intro : x0:T x1:T H4:pc3 c (THead (Flat Appl) t (THead (Bind Abst) x0 x1)) u1 H5:ty3 g c (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind Abst) x0 x1) :ty3 g c t x0 H7:nf2 c (THead (Bind Abst) x0 x1) ⇒
the thesis becomes
ex2
T
λu:T.nf2 c (lift (S i) O u)
λu:T
.pc3
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O u))
u1
(H8)
by (nf2_gen_abst . . . H7)
land (nf2 c x0) (nf2 (CHead c (Bind Abst) x0) x1)
end of H8
we proceed by induction on H8 to prove
ex2
T
λu:T.nf2 c (lift (S i) O u)
λu:T
.pc3
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O u))
u1
case conj : H9:nf2 c x0 H10:nf2 (CHead c (Bind Abst) x0) x1 ⇒
the thesis becomes
ex2
T
λu:T.nf2 c (lift (S i) O u)
λu:T
.pc3
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O u))
u1
(H_y)
by (H . . H5 H1)
nf2 c (THead (Bind Abst) x0 x1)
→(ex2
T
λu:T.nf2 c (lift (S i) O u)
λu:T
.pc3
c
THeads (Flat Appl) t0 (lift (S i) O u)
THead (Bind Abst) x0 x1)
end of H_y
(H11)
by (nf2_abst_shift . . H9 . H10)
we proved nf2 c (THead (Bind Abst) x0 x1)
by (H_y previous)
ex2
T
λu:T.nf2 c (lift (S i) O u)
λu:T
.pc3
c
THeads (Flat Appl) t0 (lift (S i) O u)
THead (Bind Abst) x0 x1
end of H11
we proceed by induction on H11 to prove
ex2
T
λu:T.nf2 c (lift (S i) O u)
λu:T
.pc3
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O u))
u1
case ex_intro2 : x:T H12:nf2 c (lift (S i) O x) H13:pc3 c (THeads (Flat Appl) t0 (lift (S i) O x)) (THead (Bind Abst) x0 x1) ⇒
the thesis becomes
ex2
T
λu:T.nf2 c (lift (S i) O u)
λu:T
.pc3
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O u))
u1
by (pc3_thin_dx . . . H13 . .)
we proved
pc3
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O x))
THead (Flat Appl) t (THead (Bind Abst) x0 x1)
by (pc3_t . . . previous . H4)
we proved
pc3
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O x))
u1
by (ex_intro2 . . . . H12 previous)
ex2
T
λu:T.nf2 c (lift (S i) O u)
λu:T
.pc3
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O u))
u1
ex2
T
λu:T.nf2 c (lift (S i) O u)
λu:T
.pc3
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O u))
u1
ex2
T
λu:T.nf2 c (lift (S i) O u)
λu:T
.pc3
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O u))
u1
we proved
ex2
T
λu:T.nf2 c (lift (S i) O u)
λu:T
.pc3
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O u))
u1
that is equivalent to
ex2
T
λu:T.nf2 c (lift (S i) O u)
λu:T.pc3 c (THeads (Flat Appl) (TCons t t0) (lift (S i) O u)) u1
we proved
ty3 g c (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) u1
→(nf2 c (TLRef i)
→(nf2 c u1
→(ex2
T
λu:T.nf2 c (lift (S i) O u)
λu:T.pc3 c (THeads (Flat Appl) (TCons t t0) (lift (S i) O u)) u1)))
that is equivalent to
ty3 g c (THeads (Flat Appl) (TCons t t0) (TLRef i)) u1
→(nf2 c (TLRef i)
→(nf2 c u1
→(ex2
T
λu:T.nf2 c (lift (S i) O u)
λu:T.pc3 c (THeads (Flat Appl) (TCons t t0) (lift (S i) O u)) u1)))
∀u1:T
.∀i:nat
.ty3 g c (THeads (Flat Appl) (TCons t t0) (TLRef i)) u1
→(nf2 c (TLRef i)
→(nf2 c u1
→(ex2
T
λu:T.nf2 c (lift (S i) O u)
λu:T.pc3 c (THeads (Flat Appl) (TCons t t0) (lift (S i) O u)) u1)))
we proved
∀u1:T
.∀i:nat
.ty3 g c (THeads (Flat Appl) vs (TLRef i)) u1
→(nf2 c (TLRef i)
→(nf2 c u1
→(ex2
T
λu:T.nf2 c (lift (S i) O u)
λu:T.pc3 c (THeads (Flat Appl) vs (lift (S i) O u)) u1)))
we proved
∀g:G
.∀c:C
.∀vs:TList
.∀u1:T
.∀i:nat
.ty3 g c (THeads (Flat Appl) vs (TLRef i)) u1
→(nf2 c (TLRef i)
→(nf2 c u1
→(ex2
T
λu:T.nf2 c (lift (S i) O u)
λu:T.pc3 c (THeads (Flat Appl) vs (lift (S i) O u)) u1)))