DEFINITION pr3_iso_appls_cast()
TYPE =
∀c:C
.∀v:T
.∀t:T
.∀vs:TList
.let u1 := THeads (Flat Appl) vs (THead (Flat Cast) v t)
in ∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P)→(pr3 c (THeads (Flat Appl) vs t) u2)
BODY =
assume c: C
assume v: T
assume t: T
assume vs: TList
we proceed by induction on vs to prove
let u1 := THeads (Flat Appl) vs (THead (Flat Cast) v t)
in ∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P)→(pr3 c (THeads (Flat Appl) vs t) u2)
case TNil : ⇒
the thesis becomes
let u1 := THeads (Flat Appl) TNil (THead (Flat Cast) v t)
in ∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P)→(pr3 c (THeads (Flat Appl) TNil t) u2)
we must prove
let u1 := THeads (Flat Appl) TNil (THead (Flat Cast) v t)
in ∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P)→(pr3 c (THeads (Flat Appl) TNil t) u2)
or equivalently
∀u2:T
.pr3 c (THeads (Flat Appl) TNil (THead (Flat Cast) v t)) u2
→(iso (THeads (Flat Appl) TNil (THead (Flat Cast) v t)) u2
→∀P:Prop.P
→pr3 c (THeads (Flat Appl) TNil t) u2)
assume u2: T
we must prove
pr3 c (THeads (Flat Appl) TNil (THead (Flat Cast) v t)) u2
→(iso (THeads (Flat Appl) TNil (THead (Flat Cast) v t)) u2
→∀P:Prop.P
→pr3 c (THeads (Flat Appl) TNil t) u2)
or equivalently
pr3 c (THead (Flat Cast) v t) u2
→(iso (THeads (Flat Appl) TNil (THead (Flat Cast) v t)) u2
→∀P:Prop.P
→pr3 c (THeads (Flat Appl) TNil t) u2)
suppose H: pr3 c (THead (Flat Cast) v t) u2
we must prove
iso (THeads (Flat Appl) TNil (THead (Flat Cast) v t)) u2
→∀P:Prop.P
→pr3 c (THeads (Flat Appl) TNil t) u2
or equivalently
(iso (THead (Flat Cast) v t) u2)→∀P:Prop.P
→pr3 c (THeads (Flat Appl) TNil t) u2
suppose H0: (iso (THead (Flat Cast) v t) u2)→∀P:Prop.P
(H1)
by (pr3_gen_cast . . . . H)
or
ex3_2 T T λu2:T.λt2:T.eq T u2 (THead (Flat Cast) u2 t2) λu2:T.λ:T.pr3 c v u2 λ:T.λt2:T.pr3 c t t2
pr3 c t u2
end of H1
we proceed by induction on H1 to prove pr3 c t u2
case or_introl : H2:ex3_2 T T λu3:T.λt2:T.eq T u2 (THead (Flat Cast) u3 t2) λu3:T.λ:T.pr3 c v u3 λ:T.λt2:T.pr3 c t t2 ⇒
the thesis becomes pr3 c t u2
we proceed by induction on H2 to prove pr3 c t u2
case ex3_2_intro : x0:T x1:T H3:eq T u2 (THead (Flat Cast) x0 x1) :pr3 c v x0 :pr3 c t x1 ⇒
the thesis becomes pr3 c t u2
(H6)
we proceed by induction on H3 to prove
iso (THead (Flat Cast) v t) (THead (Flat Cast) x0 x1)
→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes the hypothesis H0
iso (THead (Flat Cast) v t) (THead (Flat Cast) x0 x1)
→∀P:Prop.P
end of H6
by (iso_head . . . . .)
we proved iso (THead (Flat Cast) v t) (THead (Flat Cast) x0 x1)
by (H6 previous .)
we proved pr3 c t (THead (Flat Cast) x0 x1)
by (eq_ind_r . . . previous . H3)
pr3 c t u2
pr3 c t u2
case or_intror : H2:pr3 c t u2 ⇒
the thesis becomes the hypothesis H2
we proved pr3 c t u2
that is equivalent to pr3 c (THeads (Flat Appl) TNil t) u2
we proved
(iso (THead (Flat Cast) v t) u2)→∀P:Prop.P
→pr3 c (THeads (Flat Appl) TNil t) u2
that is equivalent to
iso (THeads (Flat Appl) TNil (THead (Flat Cast) v t)) u2
→∀P:Prop.P
→pr3 c (THeads (Flat Appl) TNil t) u2
we proved
pr3 c (THead (Flat Cast) v t) u2
→(iso (THeads (Flat Appl) TNil (THead (Flat Cast) v t)) u2
→∀P:Prop.P
→pr3 c (THeads (Flat Appl) TNil t) u2)
that is equivalent to
pr3 c (THeads (Flat Appl) TNil (THead (Flat Cast) v t)) u2
→(iso (THeads (Flat Appl) TNil (THead (Flat Cast) v t)) u2
→∀P:Prop.P
→pr3 c (THeads (Flat Appl) TNil t) u2)
we proved
∀u2:T
.pr3 c (THeads (Flat Appl) TNil (THead (Flat Cast) v t)) u2
→(iso (THeads (Flat Appl) TNil (THead (Flat Cast) v t)) u2
→∀P:Prop.P
→pr3 c (THeads (Flat Appl) TNil t) u2)
let u1 := THeads (Flat Appl) TNil (THead (Flat Cast) v t)
in ∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P)→(pr3 c (THeads (Flat Appl) TNil t) u2)
case TCons : t0:T t1:TList ⇒
the thesis becomes
let u1 := THeads (Flat Appl) (TCons t0 t1) (THead (Flat Cast) v t)
in ∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P)→(pr3 c (THeads (Flat Appl) (TCons t0 t1) t) u2)
(H) by induction hypothesis we know
∀u2:T
.pr3 c (THeads (Flat Appl) t1 (THead (Flat Cast) v t)) u2
→(iso (THeads (Flat Appl) t1 (THead (Flat Cast) v t)) u2
→∀P:Prop.P
→pr3 c (THeads (Flat Appl) t1 t) u2)
we must prove
let u1 := THeads (Flat Appl) (TCons t0 t1) (THead (Flat Cast) v t)
in ∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P)→(pr3 c (THeads (Flat Appl) (TCons t0 t1) t) u2)
or equivalently
∀u2:T
.pr3 c (THeads (Flat Appl) (TCons t0 t1) (THead (Flat Cast) v t)) u2
→(iso (THeads (Flat Appl) (TCons t0 t1) (THead (Flat Cast) v t)) u2
→∀P:Prop.P
→pr3 c (THeads (Flat Appl) (TCons t0 t1) t) u2)
assume u2: T
we must prove
pr3 c (THeads (Flat Appl) (TCons t0 t1) (THead (Flat Cast) v t)) u2
→(iso (THeads (Flat Appl) (TCons t0 t1) (THead (Flat Cast) v t)) u2
→∀P:Prop.P
→pr3 c (THeads (Flat Appl) (TCons t0 t1) t) u2)
or equivalently
(pr3
c
THead
Flat Appl
t0
THeads (Flat Appl) t1 (THead (Flat Cast) v t)
u2)
→(iso (THeads (Flat Appl) (TCons t0 t1) (THead (Flat Cast) v t)) u2
→∀P:Prop.P
→pr3 c (THeads (Flat Appl) (TCons t0 t1) t) u2)
suppose H0:
pr3
c
THead
Flat Appl
t0
THeads (Flat Appl) t1 (THead (Flat Cast) v t)
u2
we must prove
iso (THeads (Flat Appl) (TCons t0 t1) (THead (Flat Cast) v t)) u2
→∀P:Prop.P
→pr3 c (THeads (Flat Appl) (TCons t0 t1) t) u2
or equivalently
(iso
THead
Flat Appl
t0
THeads (Flat Appl) t1 (THead (Flat Cast) v t)
u2)
→∀P:Prop.P
→pr3 c (THeads (Flat Appl) (TCons t0 t1) t) u2
suppose H1:
(iso
THead
Flat Appl
t0
THeads (Flat Appl) t1 (THead (Flat Cast) v t)
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 t0 u2
λ:T.λt2:T.pr3 c (THeads (Flat Appl) t1 (THead (Flat Cast) v 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 Cast) v 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 Cast) v 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 H2
we proceed by induction on H2 to prove pr3 c (THead (Flat Appl) t0 (THeads (Flat Appl) t1 t)) 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 t0 u3 λ:T.λt2:T.pr3 c (THeads (Flat Appl) t1 (THead (Flat Cast) v t)) t2 ⇒
the thesis becomes pr3 c (THead (Flat Appl) t0 (THeads (Flat Appl) t1 t)) u2
we proceed by induction on H3 to prove pr3 c (THead (Flat Appl) t0 (THeads (Flat Appl) t1 t)) u2
case ex3_2_intro : x0:T x1:T H4:eq T u2 (THead (Flat Appl) x0 x1) :pr3 c t0 x0 :pr3 c (THeads (Flat Appl) t1 (THead (Flat Cast) v t)) x1 ⇒
the thesis becomes pr3 c (THead (Flat Appl) t0 (THeads (Flat Appl) t1 t)) u2
(H7)
we proceed by induction on H4 to prove
(iso
THead
Flat Appl
t0
THeads (Flat Appl) t1 (THead (Flat Cast) v t)
THead (Flat Appl) x0 x1)
→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes the hypothesis H1
(iso
THead
Flat Appl
t0
THeads (Flat Appl) t1 (THead (Flat Cast) v t)
THead (Flat Appl) x0 x1)
→∀P:Prop.P
end of H7
by (iso_head . . . . .)
we proved
iso
THead
Flat Appl
t0
THeads (Flat Appl) t1 (THead (Flat Cast) v t)
THead (Flat Appl) x0 x1
by (H7 previous .)
we proved
pr3
c
THead (Flat Appl) t0 (THeads (Flat Appl) t1 t)
THead (Flat Appl) x0 x1
by (eq_ind_r . . . previous . H4)
pr3 c (THead (Flat Appl) t0 (THeads (Flat Appl) t1 t)) u2
pr3 c (THead (Flat Appl) t0 (THeads (Flat Appl) t1 t)) 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 t0 u3 λy1:T.λz1:T.λ:T.λ:T.pr3 c (THeads (Flat Appl) t1 (THead (Flat Cast) v t)) (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) t0 (THeads (Flat Appl) t1 t)) u2
we proceed by induction on H3 to prove pr3 c (THead (Flat Appl) t0 (THeads (Flat Appl) t1 t)) 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 t0 x2 H6:pr3 c (THeads (Flat Appl) t1 (THead (Flat Cast) v t)) (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) t0 (THeads (Flat Appl) t1 t)) u2
(h1)
(h1)
suppose H8:
iso
THeads (Flat Appl) t1 (THead (Flat Cast) v t)
THead (Bind Abst) x0 x1
assume P: Prop
by (iso_flats_flat_bind_false . . . . . . . . H8 .)
we proved P
we proved
(iso
THeads (Flat Appl) t1 (THead (Flat Cast) v t)
THead (Bind Abst) x0 x1)
→∀P:Prop.P
by (H . H6 previous)
we proved pr3 c (THeads (Flat Appl) t1 t) (THead (Bind Abst) x0 x1)
by (pr3_thin_dx . . . previous . .)
pr3
c
THead (Flat Appl) t0 (THeads (Flat Appl) t1 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 t)
THead (Bind Abbr) t0 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) t0 x1) (THead (Bind Abbr) x2 x3)
by (pr3_t . . . previous . H4)
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 t)) u2
pr3 c (THead (Flat Appl) t0 (THeads (Flat Appl) t1 t)) 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) t1 (THead (Flat Cast) v t)) (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 t0 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) t0 (THeads (Flat Appl) t1 t)) u2
we proceed by induction on H3 to prove pr3 c (THead (Flat Appl) t0 (THeads (Flat Appl) t1 t)) 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) t1 (THead (Flat Cast) v t)) (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 t0 x4 H8:pr3 c x1 x5 H9:pr3 (CHead c (Bind x0) x5) x2 x3 ⇒
the thesis becomes pr3 c (THead (Flat Appl) t0 (THeads (Flat Appl) t1 t)) u2
(h1)
(h1)
(h1)
suppose H10:
iso
THeads (Flat Appl) t1 (THead (Flat Cast) v t)
THead (Bind x0) x1 x2
assume P: Prop
by (iso_flats_flat_bind_false . . . . . . . . H10 .)
we proved P
we proved
(iso
THeads (Flat Appl) t1 (THead (Flat Cast) v t)
THead (Bind x0) x1 x2)
→∀P:Prop.P
by (H . H5 previous)
we proved pr3 c (THeads (Flat Appl) t1 t) (THead (Bind x0) x1 x2)
by (pr3_thin_dx . . . previous . .)
pr3
c
THead (Flat Appl) t0 (THeads (Flat Appl) t1 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 . H4 . . 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 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 . . H7)
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 t)
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) t0 (THeads (Flat Appl) t1 t)) u2
pr3 c (THead (Flat Appl) t0 (THeads (Flat Appl) t1 t)) u2
we proved pr3 c (THead (Flat Appl) t0 (THeads (Flat Appl) t1 t)) u2
that is equivalent to pr3 c (THeads (Flat Appl) (TCons t0 t1) t) u2
we proved
(iso
THead
Flat Appl
t0
THeads (Flat Appl) t1 (THead (Flat Cast) v t)
u2)
→∀P:Prop.P
→pr3 c (THeads (Flat Appl) (TCons t0 t1) t) u2
that is equivalent to
iso (THeads (Flat Appl) (TCons t0 t1) (THead (Flat Cast) v t)) u2
→∀P:Prop.P
→pr3 c (THeads (Flat Appl) (TCons t0 t1) t) u2
we proved
(pr3
c
THead
Flat Appl
t0
THeads (Flat Appl) t1 (THead (Flat Cast) v t)
u2)
→(iso (THeads (Flat Appl) (TCons t0 t1) (THead (Flat Cast) v t)) u2
→∀P:Prop.P
→pr3 c (THeads (Flat Appl) (TCons t0 t1) t) u2)
that is equivalent to
pr3 c (THeads (Flat Appl) (TCons t0 t1) (THead (Flat Cast) v t)) u2
→(iso (THeads (Flat Appl) (TCons t0 t1) (THead (Flat Cast) v t)) u2
→∀P:Prop.P
→pr3 c (THeads (Flat Appl) (TCons t0 t1) t) u2)
we proved
∀u2:T
.pr3 c (THeads (Flat Appl) (TCons t0 t1) (THead (Flat Cast) v t)) u2
→(iso (THeads (Flat Appl) (TCons t0 t1) (THead (Flat Cast) v t)) u2
→∀P:Prop.P
→pr3 c (THeads (Flat Appl) (TCons t0 t1) t) u2)
let u1 := THeads (Flat Appl) (TCons t0 t1) (THead (Flat Cast) v t)
in ∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P)→(pr3 c (THeads (Flat Appl) (TCons t0 t1) t) u2)
we proved
let u1 := THeads (Flat Appl) vs (THead (Flat Cast) v t)
in ∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P)→(pr3 c (THeads (Flat Appl) vs t) u2)
we proved
∀c:C
.∀v:T
.∀t:T
.∀vs:TList
.let u1 := THeads (Flat Appl) vs (THead (Flat Cast) v t)
in ∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P)→(pr3 c (THeads (Flat Appl) vs t) u2)