DEFINITION nf2_iso_appls_lref()
TYPE =
∀c:C
.∀i:nat
.nf2 c (TLRef i)
→∀vs:TList
.∀u:T
.pr3 c (THeads (Flat Appl) vs (TLRef i)) u
→iso (THeads (Flat Appl) vs (TLRef i)) u
BODY =
assume c: C
assume i: nat
suppose H: nf2 c (TLRef i)
assume vs: TList
we proceed by induction on vs to prove
∀u:T
.pr3 c (THeads (Flat Appl) vs (TLRef i)) u
→iso (THeads (Flat Appl) vs (TLRef i)) u
case TNil : ⇒
the thesis becomes
∀u:T
.pr3 c (THeads (Flat Appl) TNil (TLRef i)) u
→iso (THeads (Flat Appl) TNil (TLRef i)) u
assume u: T
we must prove
pr3 c (THeads (Flat Appl) TNil (TLRef i)) u
→iso (THeads (Flat Appl) TNil (TLRef i)) u
or equivalently
pr3 c (TLRef i) u
→iso (THeads (Flat Appl) TNil (TLRef i)) u
suppose H0: pr3 c (TLRef i) u
(H_y)
by (nf2_pr3_unfold . . . H0 H)
eq T (TLRef i) u
end of H_y
we proceed by induction on H_y to prove iso (TLRef i) u
case refl_equal : ⇒
the thesis becomes iso (TLRef i) (TLRef i)
by (iso_refl .)
iso (TLRef i) (TLRef i)
we proved iso (TLRef i) u
that is equivalent to iso (THeads (Flat Appl) TNil (TLRef i)) u
we proved
pr3 c (TLRef i) u
→iso (THeads (Flat Appl) TNil (TLRef i)) u
that is equivalent to
pr3 c (THeads (Flat Appl) TNil (TLRef i)) u
→iso (THeads (Flat Appl) TNil (TLRef i)) u
∀u:T
.pr3 c (THeads (Flat Appl) TNil (TLRef i)) u
→iso (THeads (Flat Appl) TNil (TLRef i)) u
case TCons : t:T t0:TList ⇒
the thesis becomes
∀u:T
.pr3 c (THeads (Flat Appl) (TCons t t0) (TLRef i)) u
→iso (THeads (Flat Appl) (TCons t t0) (TLRef i)) u
(H0) by induction hypothesis we know
∀u:T
.pr3 c (THeads (Flat Appl) t0 (TLRef i)) u
→iso (THeads (Flat Appl) t0 (TLRef i)) u
assume u: T
we must prove
pr3 c (THeads (Flat Appl) (TCons t t0) (TLRef i)) u
→iso (THeads (Flat Appl) (TCons t t0) (TLRef i)) u
or equivalently
pr3 c (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) u
→iso (THeads (Flat Appl) (TCons t t0) (TLRef i)) u
suppose H1: pr3 c (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) u
(H2)
by (pr3_gen_appl . . . . H1)
or3
ex3_2
T
T
λu2:T.λt2:T.eq T u (THead (Flat Appl) u2 t2)
λu2:T.λ:T.pr3 c t u2
λ:T.λt2:T.pr3 c (THeads (Flat Appl) t0 (TLRef i)) t2
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt2:T.pr3 c (THead (Bind Abbr) u2 t2) u
λ:T.λ:T.λu2:T.λ:T.pr3 c t u2
λy1:T
.λz1:T.λ:T.λ:T.pr3 c (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind Abst) y1 z1)
λ:T.λz1:T.λ:T.λt2:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) z1 t2)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B
.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T
.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) u
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c t u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2
end of H2
we proceed by induction on H2 to prove
iso
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
u
case or3_intro0 : H3:ex3_2 T T λu2:T.λt2:T.eq T u (THead (Flat Appl) u2 t2) λu2:T.λ:T.pr3 c t u2 λ:T.λt2:T.pr3 c (THeads (Flat Appl) t0 (TLRef i)) t2 ⇒
the thesis becomes
iso
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
u
we proceed by induction on H3 to prove
iso
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
u
case ex3_2_intro : x0:T x1:T H4:eq T u (THead (Flat Appl) x0 x1) :pr3 c t x0 :pr3 c (THeads (Flat Appl) t0 (TLRef i)) x1 ⇒
the thesis becomes
iso
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
u
by (iso_head . . . . .)
we proved
iso
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
THead (Flat Appl) x0 x1
by (eq_ind_r . . . previous . H4)
iso
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
u
iso
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
u
case or3_intro1 : H3:ex4_4 T T T T λ:T.λ:T.λu2:T.λt2:T.pr3 c (THead (Bind Abbr) u2 t2) u λ:T.λ:T.λu2:T.λ:T.pr3 c t u2 λy1:T.λz1:T.λ:T.λ:T.pr3 c (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind Abst) y1 z1) λ:T.λz1:T.λ:T.λt2:T.∀b:B.∀u0:T.(pr3 (CHead c (Bind b) u0) z1 t2) ⇒
the thesis becomes
iso
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
u
we proceed by induction on H3 to prove
iso
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
u
case ex4_4_intro : x0:T x1:T x2:T x3:T :pr3 c (THead (Bind Abbr) x2 x3) u :pr3 c t x2 H6:pr3 c (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind Abst) x0 x1) :∀b:B.∀u0:T.(pr3 (CHead c (Bind b) u0) x1 x3) ⇒
the thesis becomes
iso
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
u
(H_y)
by (H0 . H6)
iso (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind Abst) x0 x1)
end of H_y
by (iso_flats_lref_bind_false . . . . . . H_y .)
iso
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
u
iso
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
u
case or3_intro2 : H3:ex6_6 B T T T T T λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst) λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind b) y1 z1) λb:B.λ:T.λ:T.λz2:T.λu2:T.λy2:T.pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) u λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c t u2 λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2 λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b) y2) z1 z2 ⇒
the thesis becomes
iso
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
u
we proceed by induction on H3 to prove
iso
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
u
case ex6_6_intro : x0:B x1:T x2:T x3:T x4:T x5:T :not (eq B x0 Abst) H5:pr3 c (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind x0) x1 x2) :pr3 c (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)) u :pr3 c t x4 :pr3 c x1 x5 :pr3 (CHead c (Bind x0) x5) x2 x3 ⇒
the thesis becomes
iso
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
u
(H_y)
by (H0 . H5)
iso (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind x0) x1 x2)
end of H_y
by (iso_flats_lref_bind_false . . . . . . H_y .)
iso
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
u
iso
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
u
we proved
iso
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
u
that is equivalent to iso (THeads (Flat Appl) (TCons t t0) (TLRef i)) u
we proved
pr3 c (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) u
→iso (THeads (Flat Appl) (TCons t t0) (TLRef i)) u
that is equivalent to
pr3 c (THeads (Flat Appl) (TCons t t0) (TLRef i)) u
→iso (THeads (Flat Appl) (TCons t t0) (TLRef i)) u
∀u:T
.pr3 c (THeads (Flat Appl) (TCons t t0) (TLRef i)) u
→iso (THeads (Flat Appl) (TCons t t0) (TLRef i)) u
we proved
∀u:T
.pr3 c (THeads (Flat Appl) vs (TLRef i)) u
→iso (THeads (Flat Appl) vs (TLRef i)) u
we proved
∀c:C
.∀i:nat
.nf2 c (TLRef i)
→∀vs:TList
.∀u:T
.pr3 c (THeads (Flat Appl) vs (TLRef i)) u
→iso (THeads (Flat Appl) vs (TLRef i)) u