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