DEFINITION pr3_iso_appls_appl_bind()
TYPE =
∀b:B
.not (eq B b Abst)
→∀v:T
.∀u:T
.∀t:T
.∀vs:TList
.let u1 := THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind b) u t)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→(pr3
c
THeads
Flat Appl
vs
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2))
BODY =
assume b: B
suppose H: not (eq B b Abst)
assume v: T
assume u: T
assume t: T
assume vs: TList
we proceed by induction on vs to prove
let u1 := THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind b) u t)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→(pr3
c
THeads
Flat Appl
vs
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2))
case TNil : ⇒
the thesis becomes
let u1 := THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind b) u t)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→(pr3
c
THeads
Flat Appl
TNil
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2))
we must prove
let u1 := THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind b) u t)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→(pr3
c
THeads
Flat Appl
TNil
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2))
or equivalently
∀c:C
.∀u2:T
.(pr3
c
THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind b) u t)
u2)
→((iso
THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind b) u t)
u2)
→∀P:Prop.P
→(pr3
c
THeads
Flat Appl
TNil
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2))
assume c: C
assume u2: T
we must prove
(pr3
c
THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind b) u t)
u2)
→((iso
THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind b) u t)
u2)
→∀P:Prop.P
→(pr3
c
THeads
Flat Appl
TNil
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2))
or equivalently
pr3 c (THead (Flat Appl) v (THead (Bind b) u t)) u2
→((iso
THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind b) u t)
u2)
→∀P:Prop.P
→(pr3
c
THeads
Flat Appl
TNil
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2))
suppose H0: pr3 c (THead (Flat Appl) v (THead (Bind b) u t)) u2
we must prove
(iso
THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind b) u t)
u2)
→∀P:Prop.P
→(pr3
c
THeads
Flat Appl
TNil
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2)
or equivalently
(iso (THead (Flat Appl) v (THead (Bind b) u t)) u2)→∀P:Prop.P
→(pr3
c
THeads
Flat Appl
TNil
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2)
suppose H1:
(iso (THead (Flat Appl) v (THead (Bind b) u t)) u2)→∀P:Prop.P
by (pr3_iso_appl_bind . H . . . . . H0 H1)
we proved
pr3 c (THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)) u2
that is equivalent to
pr3
c
THeads
Flat Appl
TNil
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2
we proved
(iso (THead (Flat Appl) v (THead (Bind b) u t)) u2)→∀P:Prop.P
→(pr3
c
THeads
Flat Appl
TNil
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2)
that is equivalent to
(iso
THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind b) u t)
u2)
→∀P:Prop.P
→(pr3
c
THeads
Flat Appl
TNil
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2)
we proved
pr3 c (THead (Flat Appl) v (THead (Bind b) u t)) u2
→((iso
THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind b) u t)
u2)
→∀P:Prop.P
→(pr3
c
THeads
Flat Appl
TNil
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2))
that is equivalent to
(pr3
c
THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind b) u t)
u2)
→((iso
THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind b) u t)
u2)
→∀P:Prop.P
→(pr3
c
THeads
Flat Appl
TNil
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2))
we proved
∀c:C
.∀u2:T
.(pr3
c
THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind b) u t)
u2)
→((iso
THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind b) u t)
u2)
→∀P:Prop.P
→(pr3
c
THeads
Flat Appl
TNil
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2))
let u1 := THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind b) u t)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→(pr3
c
THeads
Flat Appl
TNil
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2))
case TCons : t0:T t1:TList ⇒
the thesis becomes
let u1 := THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind b) u t)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→(pr3
c
THeads
Flat Appl
TCons t0 t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2))
(H0) by induction hypothesis we know
∀c:C
.∀u2:T
.(pr3
c
THeads
Flat Appl
t1
THead (Flat Appl) v (THead (Bind b) u t)
u2)
→((iso
THeads
Flat Appl
t1
THead (Flat Appl) v (THead (Bind b) u t)
u2)
→∀P:Prop.P
→(pr3
c
THeads
Flat Appl
t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2))
we must prove
let u1 := THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind b) u t)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→(pr3
c
THeads
Flat Appl
TCons t0 t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2))
or equivalently
∀c:C
.∀u2:T
.(pr3
c
THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind b) u t)
u2)
→((iso
THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind b) u t)
u2)
→∀P:Prop.P
→(pr3
c
THeads
Flat Appl
TCons t0 t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2))
assume c: C
assume u2: T
we must prove
(pr3
c
THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind b) u t)
u2)
→((iso
THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind b) u t)
u2)
→∀P:Prop.P
→(pr3
c
THeads
Flat Appl
TCons t0 t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2))
or equivalently
(pr3
c
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Flat Appl) v (THead (Bind b) u t)
u2)
→((iso
THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind b) u t)
u2)
→∀P:Prop.P
→(pr3
c
THeads
Flat Appl
TCons t0 t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2))
suppose H1:
pr3
c
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Flat Appl) v (THead (Bind b) u t)
u2
we must prove
(iso
THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind b) u t)
u2)
→∀P:Prop.P
→(pr3
c
THeads
Flat Appl
TCons t0 t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2)
or equivalently
(iso
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Flat Appl) v (THead (Bind b) u t)
u2)
→∀P:Prop.P
→(pr3
c
THeads
Flat Appl
TCons t0 t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2)
suppose H2:
(iso
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Flat Appl) v (THead (Bind b) u t)
u2)
→∀P:Prop.P
(H3)
by (pr3_gen_appl . . . . H1)
or3
ex3_2
T
T
λu2:T.λt2:T.eq T u2 (THead (Flat Appl) u2 t2)
λu2:T.λ:T.pr3 c t0 u2
λ:T
.λt2:T
.pr3
c
THeads
Flat Appl
t1
THead (Flat Appl) v (THead (Bind b) u t)
t2
ex4_4
T
T
T
T
λ:T.λ:T.λu2:T.λt2:T.pr3 c (THead (Bind Abbr) u2 t2) u2
λ:T.λ:T.λu2:T.λ:T.pr3 c t0 u2
λy1:T
.λz1:T
.λ:T
.λ:T
.pr3
c
THeads
Flat Appl
t1
THead (Flat Appl) v (THead (Bind b) u t)
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
t1
THead (Flat Appl) v (THead (Bind b) u t)
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)) u2
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr3 c t0 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 H3
we proceed by induction on H3 to prove
pr3
c
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2
case or3_intro0 : H4:ex3_2 T T λu3:T.λt2:T.eq T u2 (THead (Flat Appl) u3 t2) λu3:T.λ:T.pr3 c t0 u3 λ:T.λt2:T.pr3 c (THeads (Flat Appl) t1 (THead (Flat Appl) v (THead (Bind b) u t))) t2 ⇒
the thesis becomes
pr3
c
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2
we proceed by induction on H4 to prove
pr3
c
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2
case ex3_2_intro : x0:T x1:T H5:eq T u2 (THead (Flat Appl) x0 x1) :pr3 c t0 x0 :pr3 c (THeads (Flat Appl) t1 (THead (Flat Appl) v (THead (Bind b) u t))) x1 ⇒
the thesis becomes
pr3
c
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2
(H8)
we proceed by induction on H5 to prove
(iso
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Flat Appl) v (THead (Bind b) u t)
THead (Flat Appl) x0 x1)
→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes the hypothesis H2
(iso
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Flat Appl) v (THead (Bind b) u t)
THead (Flat Appl) x0 x1)
→∀P:Prop.P
end of H8
by (iso_head . . . . .)
we proved
iso
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Flat Appl) v (THead (Bind b) u t)
THead (Flat Appl) x0 x1
by (H8 previous .)
we proved
pr3
c
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
THead (Flat Appl) x0 x1
by (eq_ind_r . . . previous . H5)
pr3
c
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2
pr3
c
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2
case or3_intro1 : H4:ex4_4 T T T T λ:T.λ:T.λu3:T.λt2:T.pr3 c (THead (Bind Abbr) u3 t2) u2 λ:T.λ:T.λu3:T.λ:T.pr3 c t0 u3 λy1:T.λz1:T.λ:T.λ:T.pr3 c (THeads (Flat Appl) t1 (THead (Flat Appl) v (THead (Bind b) u t))) (THead (Bind Abst) y1 z1) λ:T.λz1:T.λ:T.λt2:T.∀b0:B.∀u0:T.(pr3 (CHead c (Bind b0) u0) z1 t2) ⇒
the thesis becomes
pr3
c
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2
we proceed by induction on H4 to prove
pr3
c
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2
case ex4_4_intro : x0:T x1:T x2:T x3:T H5:pr3 c (THead (Bind Abbr) x2 x3) u2 H6:pr3 c t0 x2 H7:pr3 c (THeads (Flat Appl) t1 (THead (Flat Appl) v (THead (Bind b) u t))) (THead (Bind Abst) x0 x1) H8:∀b0:B.∀u0:T.(pr3 (CHead c (Bind b0) u0) x1 x3) ⇒
the thesis becomes
pr3
c
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2
(h1)
(h1)
suppose H9:
iso
THeads
Flat Appl
t1
THead (Flat Appl) v (THead (Bind b) u t)
THead (Bind Abst) x0 x1
assume P: Prop
by (iso_flats_flat_bind_false . . . . . . . . H9 .)
we proved P
we proved
(iso
THeads
Flat Appl
t1
THead (Flat Appl) v (THead (Bind b) u t)
THead (Bind Abst) x0 x1)
→∀P:Prop.P
by (H0 . . H7 previous)
we proved
pr3
c
THeads
Flat Appl
t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
THead (Bind Abst) x0 x1
by (pr3_thin_dx . . . previous . .)
pr3
c
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
THead (Flat Appl) t0 (THead (Bind Abst) x0 x1)
end of h1
(h2)
(h1) by (pr0_refl .) we proved pr0 t0 t0
(h2) by (pr0_refl .) we proved pr0 x1 x1
by (pr0_beta . . . h1 . . h2)
we proved
pr0
THead (Flat Appl) t0 (THead (Bind Abst) x0 x1)
THead (Bind Abbr) t0 x1
by (pr2_free . . . previous)
we proved
pr2
c
THead (Flat Appl) t0 (THead (Bind Abst) x0 x1)
THead (Bind Abbr) t0 x1
by (pr3_pr2 . . . previous)
pr3
c
THead (Flat Appl) t0 (THead (Bind Abst) x0 x1)
THead (Bind Abbr) t0 x1
end of h2
by (pr3_t . . . h1 . h2)
pr3
c
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
THead (Bind Abbr) t0 x1
end of h1
(h2)
by (H8 . .)
we proved pr3 (CHead c (Bind Abbr) x2) x1 x3
by (pr3_head_12 . . . H6 . . . previous)
we proved pr3 c (THead (Bind Abbr) t0 x1) (THead (Bind Abbr) x2 x3)
by (pr3_t . . . previous . H5)
pr3 c (THead (Bind Abbr) t0 x1) u2
end of h2
by (pr3_t . . . h1 . h2)
pr3
c
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2
pr3
c
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2
case or3_intro2 : H4:ex6_6 B T T T T T λb0:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b0 Abst) λb0:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.pr3 c (THeads (Flat Appl) t1 (THead (Flat Appl) v (THead (Bind b) u t))) (THead (Bind b0) y1 z1) λb0:B.λ:T.λ:T.λz2:T.λu3:T.λy2:T.pr3 c (THead (Bind b0) y2 (THead (Flat Appl) (lift (S O) O u3) z2)) u2 λ:B.λ:T.λ:T.λ:T.λu3:T.λ:T.pr3 c t0 u3 λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr3 c y1 y2 λb0:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr3 (CHead c (Bind b0) y2) z1 z2 ⇒
the thesis becomes
pr3
c
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2
we proceed by induction on H4 to prove
pr3
c
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2
case ex6_6_intro : x0:B x1:T x2:T x3:T x4:T x5:T H5:not (eq B x0 Abst) H6:pr3 c (THeads (Flat Appl) t1 (THead (Flat Appl) v (THead (Bind b) u t))) (THead (Bind x0) x1 x2) H7:pr3 c (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)) u2 H8:pr3 c t0 x4 H9:pr3 c x1 x5 H10:pr3 (CHead c (Bind x0) x5) x2 x3 ⇒
the thesis becomes
pr3
c
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2
(h1)
(h1)
(h1)
suppose H11:
iso
THeads
Flat Appl
t1
THead (Flat Appl) v (THead (Bind b) u t)
THead (Bind x0) x1 x2
assume P: Prop
by (iso_flats_flat_bind_false . . . . . . . . H11 .)
we proved P
we proved
(iso
THeads
Flat Appl
t1
THead (Flat Appl) v (THead (Bind b) u t)
THead (Bind x0) x1 x2)
→∀P:Prop.P
by (H0 . . H6 previous)
we proved
pr3
c
THeads
Flat Appl
t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
THead (Bind x0) x1 x2
by (pr3_thin_dx . . . previous . .)
pr3
c
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
THead (Flat Appl) t0 (THead (Bind x0) x1 x2)
end of h1
(h2)
(h1) by (pr0_refl .) we proved pr0 t0 t0
(h2) by (pr0_refl .) we proved pr0 x1 x1
(h3) by (pr0_refl .) we proved pr0 x2 x2
by (pr0_upsilon . H5 . . h1 . . h2 . . h3)
we proved
pr0
THead (Flat Appl) t0 (THead (Bind x0) x1 x2)
THead (Bind x0) x1 (THead (Flat Appl) (lift (S O) O t0) x2)
by (pr2_free . . . previous)
we proved
pr2
c
THead (Flat Appl) t0 (THead (Bind x0) x1 x2)
THead (Bind x0) x1 (THead (Flat Appl) (lift (S O) O t0) x2)
by (pr3_pr2 . . . previous)
pr3
c
THead (Flat Appl) t0 (THead (Bind x0) x1 x2)
THead (Bind x0) x1 (THead (Flat Appl) (lift (S O) O t0) x2)
end of h2
by (pr3_t . . . h1 . h2)
pr3
c
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
THead (Bind x0) x1 (THead (Flat Appl) (lift (S O) O t0) x2)
end of h1
(h2)
(h1) by (pr3_refl . .) we proved pr3 c x1 x1
(h2)
(h1)
by (drop_refl .)
we proved drop O O c c
that is equivalent to drop (r (Bind x0) O) O c c
by (drop_drop . . . . previous .)
we proved drop (S O) O (CHead c (Bind x0) x1) c
by (pr3_lift . . . . previous . . H8)
pr3 (CHead c (Bind x0) x1) (lift (S O) O t0) (lift (S O) O x4)
end of h1
(h2)
by (pr3_refl . .)
pr3 (CHead (CHead c (Bind x0) x1) (Flat Appl) (lift (S O) O x4)) x2 x2
end of h2
by (pr3_head_12 . . . h1 . . . h2)
pr3
CHead c (Bind x0) x1
THead (Flat Appl) (lift (S O) O t0) x2
THead (Flat Appl) (lift (S O) O x4) x2
end of h2
by (pr3_head_12 . . . h1 . . . h2)
pr3
c
THead (Bind x0) x1 (THead (Flat Appl) (lift (S O) O t0) x2)
THead (Bind x0) x1 (THead (Flat Appl) (lift (S O) O x4) x2)
end of h2
by (pr3_t . . . h1 . h2)
pr3
c
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
THead (Bind x0) x1 (THead (Flat Appl) (lift (S O) O x4) x2)
end of h1
(h2)
by (pr3_thin_dx . . . H10 . .)
we proved
pr3
CHead c (Bind x0) x5
THead (Flat Appl) (lift (S O) O x4) x2
THead (Flat Appl) (lift (S O) O x4) x3
by (pr3_head_12 . . . H9 . . . previous)
we proved
pr3
c
THead (Bind x0) x1 (THead (Flat Appl) (lift (S O) O x4) x2)
THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)
by (pr3_t . . . previous . H7)
pr3 c (THead (Bind x0) x1 (THead (Flat Appl) (lift (S O) O x4) x2)) u2
end of h2
by (pr3_t . . . h1 . h2)
pr3
c
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2
pr3
c
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2
we proved
pr3
c
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2
that is equivalent to
pr3
c
THeads
Flat Appl
TCons t0 t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2
we proved
(iso
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Flat Appl) v (THead (Bind b) u t)
u2)
→∀P:Prop.P
→(pr3
c
THeads
Flat Appl
TCons t0 t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2)
that is equivalent to
(iso
THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind b) u t)
u2)
→∀P:Prop.P
→(pr3
c
THeads
Flat Appl
TCons t0 t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2)
we proved
(pr3
c
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Flat Appl) v (THead (Bind b) u t)
u2)
→((iso
THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind b) u t)
u2)
→∀P:Prop.P
→(pr3
c
THeads
Flat Appl
TCons t0 t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2))
that is equivalent to
(pr3
c
THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind b) u t)
u2)
→((iso
THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind b) u t)
u2)
→∀P:Prop.P
→(pr3
c
THeads
Flat Appl
TCons t0 t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2))
we proved
∀c:C
.∀u2:T
.(pr3
c
THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind b) u t)
u2)
→((iso
THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind b) u t)
u2)
→∀P:Prop.P
→(pr3
c
THeads
Flat Appl
TCons t0 t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2))
let u1 := THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind b) u t)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→(pr3
c
THeads
Flat Appl
TCons t0 t1
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2))
we proved
let u1 := THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind b) u t)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→(pr3
c
THeads
Flat Appl
vs
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2))
we proved
∀b:B
.not (eq B b Abst)
→∀v:T
.∀u:T
.∀t:T
.∀vs:TList
.let u1 := THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind b) u t)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→(pr3
c
THeads
Flat Appl
vs
THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t)
u2))