DEFINITION pr3_iso_appls_abbr()
TYPE =
∀c:C
.∀d:C
.∀w:T
.∀i:nat
.getl i c (CHead d (Bind Abbr) w)
→∀vs:TList
.let u1 := THeads (Flat Appl) vs (TLRef i)
in ∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→pr3 c (THeads (Flat Appl) vs (lift (S i) O w)) u2)
BODY =
assume c: C
assume d: C
assume w: T
assume i: nat
suppose H: getl i c (CHead d (Bind Abbr) w)
assume vs: TList
we proceed by induction on vs to prove
let u1 := THeads (Flat Appl) vs (TLRef i)
in ∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→pr3 c (THeads (Flat Appl) vs (lift (S i) O w)) u2)
case TNil : ⇒
the thesis becomes
let u1 := THeads (Flat Appl) TNil (TLRef i)
in ∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→pr3 c (THeads (Flat Appl) TNil (lift (S i) O w)) u2)
we must prove
let u1 := THeads (Flat Appl) TNil (TLRef i)
in ∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→pr3 c (THeads (Flat Appl) TNil (lift (S i) O w)) u2)
or equivalently
∀u2:T
.pr3 c (THeads (Flat Appl) TNil (TLRef i)) u2
→((iso (THeads (Flat Appl) TNil (TLRef i)) u2)→∀P:Prop.P
→pr3 c (THeads (Flat Appl) TNil (lift (S i) O w)) u2)
assume u2: T
we must prove
pr3 c (THeads (Flat Appl) TNil (TLRef i)) u2
→((iso (THeads (Flat Appl) TNil (TLRef i)) u2)→∀P:Prop.P
→pr3 c (THeads (Flat Appl) TNil (lift (S i) O w)) u2)
or equivalently
pr3 c (TLRef i) u2
→((iso (THeads (Flat Appl) TNil (TLRef i)) u2)→∀P:Prop.P
→pr3 c (THeads (Flat Appl) TNil (lift (S i) O w)) u2)
suppose H0: pr3 c (TLRef i) u2
we must prove
(iso (THeads (Flat Appl) TNil (TLRef i)) u2)→∀P:Prop.P
→pr3 c (THeads (Flat Appl) TNil (lift (S i) O w)) u2
or equivalently
(iso (TLRef i) u2)→∀P:Prop.P
→pr3 c (THeads (Flat Appl) TNil (lift (S i) O w)) u2
suppose H1: (iso (TLRef i) u2)→∀P:Prop.P
(H2)
by (pr3_gen_lref . . . H0)
or
eq T u2 (TLRef i)
ex3_3
C
T
T
λd:C.λu:T.λ:T.getl i c (CHead d (Bind Abbr) u)
λd:C.λu:T.λv:T.pr3 d u v
λ:C.λ:T.λv:T.eq T u2 (lift (S i) O v)
end of H2
we proceed by induction on H2 to prove pr3 c (lift (S i) O w) u2
case or_introl : H3:eq T u2 (TLRef i) ⇒
the thesis becomes pr3 c (lift (S i) O w) u2
(H4)
we proceed by induction on H3 to prove (iso (TLRef i) (TLRef i))→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes the hypothesis H1
(iso (TLRef i) (TLRef i))→∀P:Prop.P
end of H4
by (iso_refl .)
we proved iso (TLRef i) (TLRef i)
by (H4 previous .)
we proved pr3 c (lift (S i) O w) (TLRef i)
by (eq_ind_r . . . previous . H3)
pr3 c (lift (S i) O w) u2
case or_intror : H3:ex3_3 C T T λd0:C.λu:T.λ:T.getl i c (CHead d0 (Bind Abbr) u) λd0:C.λu:T.λv:T.pr3 d0 u v λ:C.λ:T.λv:T.eq T u2 (lift (S i) O v) ⇒
the thesis becomes pr3 c (lift (S i) O w) u2
we proceed by induction on H3 to prove pr3 c (lift (S i) O w) u2
case ex3_3_intro : x0:C x1:T x2:T H4:getl i c (CHead x0 (Bind Abbr) x1) H5:pr3 x0 x1 x2 H6:eq T u2 (lift (S i) O x2) ⇒
the thesis becomes pr3 c (lift (S i) O w) u2
(H8)
by (getl_mono . . . H . H4)
we proved eq C (CHead d (Bind Abbr) w) (CHead x0 (Bind Abbr) x1)
we proceed by induction on the previous result to prove getl i c (CHead x0 (Bind Abbr) x1)
case refl_equal : ⇒
the thesis becomes the hypothesis H
getl i c (CHead x0 (Bind Abbr) x1)
end of H8
(H9)
by (getl_mono . . . H . H4)
we proved eq C (CHead d (Bind Abbr) w) (CHead x0 (Bind Abbr) x1)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) w OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead x0 (Bind Abbr) x1 OF CSort ⇒d | CHead c0 ⇒c0
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c0 ⇒c0 (CHead d (Bind Abbr) w)
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c0 ⇒c0 (CHead x0 (Bind Abbr) x1)
end of H9
(h1)
(H10)
by (getl_mono . . . H . H4)
we proved eq C (CHead d (Bind Abbr) w) (CHead x0 (Bind Abbr) x1)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) w OF CSort ⇒w | CHead t⇒t
<λ:C.T> CASE CHead x0 (Bind Abbr) x1 OF CSort ⇒w | CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒w | CHead t⇒t (CHead d (Bind Abbr) w)
λe:C.<λ:C.T> CASE e OF CSort ⇒w | CHead t⇒t (CHead x0 (Bind Abbr) x1)
end of H10
suppose H11: eq C d x0
(H12)
consider H10
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) w OF CSort ⇒w | CHead t⇒t
<λ:C.T> CASE CHead x0 (Bind Abbr) x1 OF CSort ⇒w | CHead t⇒t
that is equivalent to eq T w x1
by (eq_ind_r . . . H8 . previous)
getl i c (CHead x0 (Bind Abbr) w)
end of H12
(H13)
consider H10
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) w OF CSort ⇒w | CHead t⇒t
<λ:C.T> CASE CHead x0 (Bind Abbr) x1 OF CSort ⇒w | CHead t⇒t
that is equivalent to eq T w x1
by (eq_ind_r . . . H5 . previous)
pr3 x0 w x2
end of H13
(H14)
by (eq_ind_r . . . H12 . H11)
getl i c (CHead d (Bind Abbr) w)
end of H14
(H15)
by (eq_ind_r . . . H13 . H11)
pr3 d w x2
end of H15
by (getl_drop . . . . . H14)
we proved drop (S i) O c d
by (pr3_lift . . . . previous . . H15)
we proved pr3 c (lift (S i) O w) (lift (S i) O x2)
(eq C d x0)→(pr3 c (lift (S i) O w) (lift (S i) O x2))
end of h1
(h2)
consider H9
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) w OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead x0 (Bind Abbr) x1 OF CSort ⇒d | CHead c0 ⇒c0
eq C d x0
end of h2
by (h1 h2)
we proved pr3 c (lift (S i) O w) (lift (S i) O x2)
by (eq_ind_r . . . previous . H6)
pr3 c (lift (S i) O w) u2
pr3 c (lift (S i) O w) u2
we proved pr3 c (lift (S i) O w) u2
that is equivalent to pr3 c (THeads (Flat Appl) TNil (lift (S i) O w)) u2
we proved
(iso (TLRef i) u2)→∀P:Prop.P
→pr3 c (THeads (Flat Appl) TNil (lift (S i) O w)) u2
that is equivalent to
(iso (THeads (Flat Appl) TNil (TLRef i)) u2)→∀P:Prop.P
→pr3 c (THeads (Flat Appl) TNil (lift (S i) O w)) u2
we proved
pr3 c (TLRef i) u2
→((iso (THeads (Flat Appl) TNil (TLRef i)) u2)→∀P:Prop.P
→pr3 c (THeads (Flat Appl) TNil (lift (S i) O w)) u2)
that is equivalent to
pr3 c (THeads (Flat Appl) TNil (TLRef i)) u2
→((iso (THeads (Flat Appl) TNil (TLRef i)) u2)→∀P:Prop.P
→pr3 c (THeads (Flat Appl) TNil (lift (S i) O w)) u2)
we proved
∀u2:T
.pr3 c (THeads (Flat Appl) TNil (TLRef i)) u2
→((iso (THeads (Flat Appl) TNil (TLRef i)) u2)→∀P:Prop.P
→pr3 c (THeads (Flat Appl) TNil (lift (S i) O w)) u2)
let u1 := THeads (Flat Appl) TNil (TLRef i)
in ∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→pr3 c (THeads (Flat Appl) TNil (lift (S i) O w)) u2)
case TCons : t:T t0:TList ⇒
the thesis becomes
let u1 := THeads (Flat Appl) (TCons t t0) (TLRef i)
in ∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→pr3 c (THeads (Flat Appl) (TCons t t0) (lift (S i) O w)) u2)
(H0) by induction hypothesis we know
∀u2:T
.pr3 c (THeads (Flat Appl) t0 (TLRef i)) u2
→((iso (THeads (Flat Appl) t0 (TLRef i)) u2)→∀P:Prop.P
→pr3 c (THeads (Flat Appl) t0 (lift (S i) O w)) u2)
we must prove
let u1 := THeads (Flat Appl) (TCons t t0) (TLRef i)
in ∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→pr3 c (THeads (Flat Appl) (TCons t t0) (lift (S i) O w)) u2)
or equivalently
∀u2:T
.pr3 c (THeads (Flat Appl) (TCons t t0) (TLRef i)) u2
→((iso (THeads (Flat Appl) (TCons t t0) (TLRef i)) u2)→∀P:Prop.P
→pr3 c (THeads (Flat Appl) (TCons t t0) (lift (S i) O w)) u2)
assume u2: T
we must prove
pr3 c (THeads (Flat Appl) (TCons t t0) (TLRef i)) u2
→((iso (THeads (Flat Appl) (TCons t t0) (TLRef i)) u2)→∀P:Prop.P
→pr3 c (THeads (Flat Appl) (TCons t t0) (lift (S i) O w)) u2)
or equivalently
pr3 c (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) u2
→((iso (THeads (Flat Appl) (TCons t t0) (TLRef i)) u2)→∀P:Prop.P
→pr3 c (THeads (Flat Appl) (TCons t t0) (lift (S i) O w)) u2)
suppose H1: pr3 c (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) u2
we must prove
(iso (THeads (Flat Appl) (TCons t t0) (TLRef i)) u2)→∀P:Prop.P
→pr3 c (THeads (Flat Appl) (TCons t t0) (lift (S i) O w)) u2
or equivalently
iso (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) u2
→∀P:Prop.P
→pr3 c (THeads (Flat Appl) (TCons t t0) (lift (S i) O w)) u2
suppose H2:
iso (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) 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 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) u2
λ: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)) 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 H3
we proceed by induction on H3 to prove
pr3
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O w))
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 t u3 λ:T.λt2:T.pr3 c (THeads (Flat Appl) t0 (TLRef i)) t2 ⇒
the thesis becomes
pr3
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O w))
u2
we proceed by induction on H4 to prove
pr3
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O w))
u2
case ex3_2_intro : x0:T x1:T H5:eq T u2 (THead (Flat Appl) x0 x1) :pr3 c t x0 :pr3 c (THeads (Flat Appl) t0 (TLRef i)) x1 ⇒
the thesis becomes
pr3
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O w))
u2
(H8)
we proceed by induction on H5 to prove
(iso
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
THead (Flat Appl) x0 x1)
→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes the hypothesis H2
(iso
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
THead (Flat Appl) x0 x1)
→∀P:Prop.P
end of H8
by (iso_head . . . . .)
we proved
iso
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
THead (Flat Appl) x0 x1
by (H8 previous .)
we proved
pr3
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O w))
THead (Flat Appl) x0 x1
by (eq_ind_r . . . previous . H5)
pr3
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O w))
u2
pr3
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O w))
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 t u3 λ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) ⇒
the thesis becomes
pr3
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O w))
u2
we proceed by induction on H4 to prove
pr3
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O w))
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 t x2 H7:pr3 c (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind Abst) x0 x1) H8:∀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 (lift (S i) O w))
u2
(h1)
(h1)
suppose H9: iso (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind Abst) x0 x1)
assume P: Prop
by (iso_flats_lref_bind_false . . . . . . H9 .)
we proved P
we proved
iso (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind Abst) x0 x1)
→∀P:Prop.P
by (H0 . H7 previous)
we proved
pr3
c
THeads (Flat Appl) t0 (lift (S i) O w)
THead (Bind Abst) x0 x1
by (pr3_thin_dx . . . previous . .)
pr3
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O w))
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 (lift (S i) O w))
THead (Bind Abbr) t 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) t x1) (THead (Bind Abbr) x2 x3)
by (pr3_t . . . previous . H5)
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 (lift (S i) O w))
u2
pr3
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O w))
u2
case or3_intro2 : H4: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.λ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 (lift (S i) O w))
u2
we proceed by induction on H4 to prove
pr3
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O w))
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) t0 (TLRef i)) (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 t x4 H9:pr3 c x1 x5 H10:pr3 (CHead c (Bind x0) x5) x2 x3 ⇒
the thesis becomes
pr3
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O w))
u2
(h1)
(h1)
(h1)
suppose H11: iso (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind x0) x1 x2)
assume P: Prop
by (iso_flats_lref_bind_false . . . . . . H11 .)
we proved P
we proved
iso (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind x0) x1 x2)
→∀P:Prop.P
by (H0 . H6 previous)
we proved pr3 c (THeads (Flat Appl) t0 (lift (S i) O w)) (THead (Bind x0) x1 x2)
by (pr3_thin_dx . . . previous . .)
pr3
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O w))
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 . H5 . . 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 (lift (S i) O w))
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 . . H8)
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 (lift (S i) O w))
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) t (THeads (Flat Appl) t0 (lift (S i) O w))
u2
pr3
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O w))
u2
we proved
pr3
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O w))
u2
that is equivalent to pr3 c (THeads (Flat Appl) (TCons t t0) (lift (S i) O w)) u2
we proved
iso (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) u2
→∀P:Prop.P
→pr3 c (THeads (Flat Appl) (TCons t t0) (lift (S i) O w)) u2
that is equivalent to
(iso (THeads (Flat Appl) (TCons t t0) (TLRef i)) u2)→∀P:Prop.P
→pr3 c (THeads (Flat Appl) (TCons t t0) (lift (S i) O w)) u2
we proved
pr3 c (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) u2
→((iso (THeads (Flat Appl) (TCons t t0) (TLRef i)) u2)→∀P:Prop.P
→pr3 c (THeads (Flat Appl) (TCons t t0) (lift (S i) O w)) u2)
that is equivalent to
pr3 c (THeads (Flat Appl) (TCons t t0) (TLRef i)) u2
→((iso (THeads (Flat Appl) (TCons t t0) (TLRef i)) u2)→∀P:Prop.P
→pr3 c (THeads (Flat Appl) (TCons t t0) (lift (S i) O w)) u2)
we proved
∀u2:T
.pr3 c (THeads (Flat Appl) (TCons t t0) (TLRef i)) u2
→((iso (THeads (Flat Appl) (TCons t t0) (TLRef i)) u2)→∀P:Prop.P
→pr3 c (THeads (Flat Appl) (TCons t t0) (lift (S i) O w)) u2)
let u1 := THeads (Flat Appl) (TCons t t0) (TLRef i)
in ∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→pr3 c (THeads (Flat Appl) (TCons t t0) (lift (S i) O w)) u2)
we proved
let u1 := THeads (Flat Appl) vs (TLRef i)
in ∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→pr3 c (THeads (Flat Appl) vs (lift (S i) O w)) u2)
we proved
∀c:C
.∀d:C
.∀w:T
.∀i:nat
.getl i c (CHead d (Bind Abbr) w)
→∀vs:TList
.let u1 := THeads (Flat Appl) vs (TLRef i)
in ∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→pr3 c (THeads (Flat Appl) vs (lift (S i) O w)) u2)