DEFINITION pr3_iso_appls_bind()
TYPE =
∀b:B
.not (eq B b Abst)
→∀vs:TList
.∀u:T
.∀t:T
.let u1 := THeads (Flat Appl) vs (THead (Bind b) u t)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→(pr3
c
THead (Bind b) u (THeads (Flat Appl) (lifts (S O) O vs) t)
u2))
BODY =
assume b: B
suppose H: not (eq B b Abst)
assume vs: TList
(h1)
assume u: T
assume t: T
we must prove
let u1 := THeads (Flat Appl) TNil (THead (Bind b) u t)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→(pr3
c
THead
Bind b
u
THeads (Flat Appl) (lifts (S O) O TNil) t
u2))
or equivalently
∀c:C
.∀u2:T
.pr3 c (THeads (Flat Appl) TNil (THead (Bind b) u t)) u2
→(iso (THeads (Flat Appl) TNil (THead (Bind b) u t)) u2
→∀P:Prop.P
→(pr3
c
THead
Bind b
u
THeads (Flat Appl) (lifts (S O) O TNil) t
u2))
assume c: C
assume u2: T
we must prove
pr3 c (THeads (Flat Appl) TNil (THead (Bind b) u t)) u2
→(iso (THeads (Flat Appl) TNil (THead (Bind b) u t)) u2
→∀P:Prop.P
→(pr3
c
THead
Bind b
u
THeads (Flat Appl) (lifts (S O) O TNil) t
u2))
or equivalently
pr3 c (THead (Bind b) u t) u2
→(iso (THeads (Flat Appl) TNil (THead (Bind b) u t)) u2
→∀P:Prop.P
→(pr3
c
THead
Bind b
u
THeads (Flat Appl) (lifts (S O) O TNil) t
u2))
suppose H0: pr3 c (THead (Bind b) u t) u2
we must prove
iso (THeads (Flat Appl) TNil (THead (Bind b) u t)) u2
→∀P:Prop.P
→(pr3
c
THead
Bind b
u
THeads (Flat Appl) (lifts (S O) O TNil) t
u2)
or equivalently
(iso (THead (Bind b) u t) u2)→∀P:Prop.P
→(pr3
c
THead
Bind b
u
THeads (Flat Appl) (lifts (S O) O TNil) t
u2)
suppose : (iso (THead (Bind b) u t) u2)→∀P:Prop.P
consider H0
we proved pr3 c (THead (Bind b) u t) u2
that is equivalent to
pr3
c
THead
Bind b
u
THeads (Flat Appl) (lifts (S O) O TNil) t
u2
we proved
(iso (THead (Bind b) u t) u2)→∀P:Prop.P
→(pr3
c
THead
Bind b
u
THeads (Flat Appl) (lifts (S O) O TNil) t
u2)
that is equivalent to
iso (THeads (Flat Appl) TNil (THead (Bind b) u t)) u2
→∀P:Prop.P
→(pr3
c
THead
Bind b
u
THeads (Flat Appl) (lifts (S O) O TNil) t
u2)
we proved
pr3 c (THead (Bind b) u t) u2
→(iso (THeads (Flat Appl) TNil (THead (Bind b) u t)) u2
→∀P:Prop.P
→(pr3
c
THead
Bind b
u
THeads (Flat Appl) (lifts (S O) O TNil) t
u2))
that is equivalent to
pr3 c (THeads (Flat Appl) TNil (THead (Bind b) u t)) u2
→(iso (THeads (Flat Appl) TNil (THead (Bind b) u t)) u2
→∀P:Prop.P
→(pr3
c
THead
Bind b
u
THeads (Flat Appl) (lifts (S O) O TNil) t
u2))
we proved
∀c:C
.∀u2:T
.pr3 c (THeads (Flat Appl) TNil (THead (Bind b) u t)) u2
→(iso (THeads (Flat Appl) TNil (THead (Bind b) u t)) u2
→∀P:Prop.P
→(pr3
c
THead
Bind b
u
THeads (Flat Appl) (lifts (S O) O TNil) t
u2))
that is equivalent to
let u1 := THeads (Flat Appl) TNil (THead (Bind b) u t)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→(pr3
c
THead
Bind b
u
THeads (Flat Appl) (lifts (S O) O TNil) t
u2))
∀u:T
.∀t:T
.let u1 := THeads (Flat Appl) TNil (THead (Bind b) u t)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→(pr3
c
THead
Bind b
u
THeads (Flat Appl) (lifts (S O) O TNil) t
u2))
end of h1
(h2)
assume ts: TList
assume t: T
we must prove
∀u:T
.∀t0:T
.let u1 := THeads (Flat Appl) ts (THead (Bind b) u t0)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→(pr3
c
THead (Bind b) u (THeads (Flat Appl) (lifts (S O) O ts) t0)
u2))
→∀u:T
.∀t0:T
.let u1 := THeads (Flat Appl) (TApp ts t) (THead (Bind b) u t0)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→(pr3
c
THead
Bind b
u
THeads (Flat Appl) (lifts (S O) O (TApp ts t)) t0
u2))
or equivalently
∀u:T
.∀t0:T
.∀c:C
.∀u2:T
.pr3 c (THeads (Flat Appl) ts (THead (Bind b) u t0)) u2
→(iso (THeads (Flat Appl) ts (THead (Bind b) u t0)) u2
→∀P:Prop.P
→(pr3
c
THead (Bind b) u (THeads (Flat Appl) (lifts (S O) O ts) t0)
u2))
→∀u:T
.∀t0:T
.let u1 := THeads (Flat Appl) (TApp ts t) (THead (Bind b) u t0)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→(pr3
c
THead
Bind b
u
THeads (Flat Appl) (lifts (S O) O (TApp ts t)) t0
u2))
suppose H0:
∀u:T
.∀t0:T
.∀c:C
.∀u2:T
.pr3 c (THeads (Flat Appl) ts (THead (Bind b) u t0)) u2
→(iso (THeads (Flat Appl) ts (THead (Bind b) u t0)) u2
→∀P:Prop.P
→(pr3
c
THead (Bind b) u (THeads (Flat Appl) (lifts (S O) O ts) t0)
u2))
assume u: T
assume t0: T
we must prove
let u1 := THeads (Flat Appl) (TApp ts t) (THead (Bind b) u t0)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→(pr3
c
THead
Bind b
u
THeads (Flat Appl) (lifts (S O) O (TApp ts t)) t0
u2))
or equivalently
∀c:C
.∀u2:T
.pr3 c (THeads (Flat Appl) (TApp ts t) (THead (Bind b) u t0)) u2
→(iso (THeads (Flat Appl) (TApp ts t) (THead (Bind b) u t0)) u2
→∀P:Prop.P
→(pr3
c
THead
Bind b
u
THeads (Flat Appl) (lifts (S O) O (TApp ts t)) t0
u2))
assume c: C
assume u2: T
suppose H1: pr3 c (THeads (Flat Appl) (TApp ts t) (THead (Bind b) u t0)) u2
suppose H2:
iso (THeads (Flat Appl) (TApp ts t) (THead (Bind b) u t0)) u2
→∀P:Prop.P
(h1)
(h1)
(H3)
by (theads_tapp . . . .)
we proved
eq
T
THeads (Flat Appl) (TApp ts t) (THead (Bind b) u t0)
THeads
Flat Appl
ts
THead (Flat Appl) t (THead (Bind b) u t0)
we proceed by induction on the previous result to prove
pr3
c
THeads
Flat Appl
ts
THead (Flat Appl) t (THead (Bind b) u t0)
u2
case refl_equal : ⇒
the thesis becomes the hypothesis H1
pr3
c
THeads
Flat Appl
ts
THead (Flat Appl) t (THead (Bind b) u t0)
u2
end of H3
(H4)
by (theads_tapp . . . .)
we proved
eq
T
THeads (Flat Appl) (TApp ts t) (THead (Bind b) u t0)
THeads
Flat Appl
ts
THead (Flat Appl) t (THead (Bind b) u t0)
we proceed by induction on the previous result to prove
(iso
THeads
Flat Appl
ts
THead (Flat Appl) t (THead (Bind b) u t0)
u2)
→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes the hypothesis H2
(iso
THeads
Flat Appl
ts
THead (Flat Appl) t (THead (Bind b) u t0)
u2)
→∀P:Prop.P
end of H4
suppose :
∀u0:T
.∀t1:T
.∀c0:C
.∀u3:T
.pr3 c0 (THeads (Flat Appl) TNil (THead (Bind b) u0 t1)) u3
→(iso (THeads (Flat Appl) TNil (THead (Bind b) u0 t1)) u3
→∀P:Prop.P
→(pr3
c0
THead (Bind b) u0 (THeads (Flat Appl) (lifts (S O) O TNil) t1)
u3))
suppose H6:
pr3
c
THeads
Flat Appl
TNil
THead (Flat Appl) t (THead (Bind b) u t0)
u2
suppose H7:
(iso
THeads
Flat Appl
TNil
THead (Flat Appl) t (THead (Bind b) u t0)
u2)
→∀P:Prop.P
(h1)
consider H6
we proved
pr3
c
THeads
Flat Appl
TNil
THead (Flat Appl) t (THead (Bind b) u t0)
u2
pr3 c (THead (Flat Appl) t (THead (Bind b) u t0)) u2
end of h1
(h2)
consider H7
we proved
(iso
THeads
Flat Appl
TNil
THead (Flat Appl) t (THead (Bind b) u t0)
u2)
→∀P:Prop.P
(iso (THead (Flat Appl) t (THead (Bind b) u t0)) u2)→∀P:Prop.P
end of h2
by (pr3_iso_appl_bind . H . . . . . h1 h2)
we proved pr3 c (THead (Bind b) u (THead (Flat Appl) (lift (S O) O t) t0)) u2
that is equivalent to
pr3
c
THead
Bind b
u
THeads
Flat Appl
lifts (S O) O TNil
THead (Flat Appl) (lift (S O) O t) t0
u2
∀u0:T
.∀t1:T
.∀c0:C
.∀u3:T
.pr3 c0 (THeads (Flat Appl) TNil (THead (Bind b) u0 t1)) u3
→(iso (THeads (Flat Appl) TNil (THead (Bind b) u0 t1)) u3
→∀P:Prop.P
→(pr3
c0
THead (Bind b) u0 (THeads (Flat Appl) (lifts (S O) O TNil) t1)
u3))
→((pr3
c
THeads
Flat Appl
TNil
THead (Flat Appl) t (THead (Bind b) u t0)
u2)
→((iso
THeads
Flat Appl
TNil
THead (Flat Appl) t (THead (Bind b) u t0)
u2)
→∀P:Prop.P
→(pr3
c
THead
Bind b
u
THeads
Flat Appl
lifts (S O) O TNil
THead (Flat Appl) (lift (S O) O t) t0
u2)))
assume t1: T
assume ts0: TList
suppose :
∀u0:T
.∀t2:T
.∀c0:C
.∀u3:T
.pr3 c0 (THeads (Flat Appl) ts0 (THead (Bind b) u0 t2)) u3
→((iso (THeads (Flat Appl) ts0 (THead (Bind b) u0 t2)) u3)→∀P:Prop.P
→pr3 c0 (THead (Bind b) u0 (THeads (Flat Appl) (lifts (S O) O ts0) t2)) u3)
→((pr3
c
THeads
Flat Appl
ts0
THead (Flat Appl) t (THead (Bind b) u t0)
u2)
→((iso
THeads
Flat Appl
ts0
THead (Flat Appl) t (THead (Bind b) u t0)
u2)
→∀P:Prop.P
→(pr3
c
THead
Bind b
u
THeads
Flat Appl
lifts (S O) O ts0
THead (Flat Appl) (lift (S O) O t) t0
u2)))
suppose H5:
∀u0:T
.∀t2:T
.∀c0:C
.∀u3:T
.pr3 c0 (THeads (Flat Appl) (TCons t1 ts0) (THead (Bind b) u0 t2)) u3
→(iso (THeads (Flat Appl) (TCons t1 ts0) (THead (Bind b) u0 t2)) u3
→∀P:Prop.P
→(pr3
c0
THead
Bind b
u0
THeads (Flat Appl) (lifts (S O) O (TCons t1 ts0)) t2
u3))
suppose H6:
pr3
c
THeads
Flat Appl
TCons t1 ts0
THead (Flat Appl) t (THead (Bind b) u t0)
u2
suppose H7:
(iso
THeads
Flat Appl
TCons t1 ts0
THead (Flat Appl) t (THead (Bind b) u t0)
u2)
→∀P:Prop.P
(h1)
by (pr3_iso_appls_appl_bind . H . . . . . . H6 H7)
pr3
c
THeads
Flat Appl
TCons t1 ts0
THead (Bind b) u (THead (Flat Appl) (lift (S O) O t) t0)
u2
end of h1
(h2)
suppose H8:
iso
THeads
Flat Appl
TCons t1 ts0
THead (Bind b) u (THead (Flat Appl) (lift (S O) O t) t0)
u2
assume P: Prop
by (iso_head . . . . .)
we proved
iso
THead
Flat Appl
t1
THeads
Flat Appl
ts0
THead (Flat Appl) t (THead (Bind b) u t0)
THead
Flat Appl
t1
THeads
Flat Appl
ts0
THead (Bind b) u (THead (Flat Appl) (lift (S O) O t) t0)
that is equivalent to
iso
THeads
Flat Appl
TCons t1 ts0
THead (Flat Appl) t (THead (Bind b) u t0)
THeads
Flat Appl
TCons t1 ts0
THead (Bind b) u (THead (Flat Appl) (lift (S O) O t) t0)
by (iso_trans . . previous . H8)
we proved
iso
THeads
Flat Appl
TCons t1 ts0
THead (Flat Appl) t (THead (Bind b) u t0)
u2
by (H7 previous .)
we proved P
(iso
THeads
Flat Appl
TCons t1 ts0
THead (Bind b) u (THead (Flat Appl) (lift (S O) O t) t0)
u2)
→∀P:Prop.P
end of h2
by (H5 . . . . h1 h2)
we proved
pr3
c
THead
Bind b
u
THeads
Flat Appl
lifts (S O) O (TCons t1 ts0)
THead (Flat Appl) (lift (S O) O t) t0
u2
∀H5:∀u0:T
.∀t2:T
.∀c0:C
.∀u3:T
.pr3 c0 (THeads (Flat Appl) (TCons t1 ts0) (THead (Bind b) u0 t2)) u3
→(iso (THeads (Flat Appl) (TCons t1 ts0) (THead (Bind b) u0 t2)) u3
→∀P:Prop.P
→(pr3
c0
THead
Bind b
u0
THeads (Flat Appl) (lifts (S O) O (TCons t1 ts0)) t2
u3))
.∀H6:pr3
c
THeads
Flat Appl
TCons t1 ts0
THead (Flat Appl) t (THead (Bind b) u t0)
u2
.∀H7:(iso
THeads
Flat Appl
TCons t1 ts0
THead (Flat Appl) t (THead (Bind b) u t0)
u2)
→∀P:Prop.P
.pr3
c
THead
Bind b
u
THeads
Flat Appl
lifts (S O) O (TCons t1 ts0)
THead (Flat Appl) (lift (S O) O t) t0
u2
by (previous . H0 H3 H4)
pr3
c
THead
Bind b
u
THeads
Flat Appl
lifts (S O) O ts
THead (Flat Appl) (lift (S O) O t) t0
u2
end of h1
(h2)
by (theads_tapp . . . .)
eq
T
THeads
Flat Appl
TApp (lifts (S O) O ts) (lift (S O) O t)
t0
THeads
Flat Appl
lifts (S O) O ts
THead (Flat Appl) (lift (S O) O t) t0
end of h2
by (eq_ind_r . . . h1 . h2)
pr3
c
THead
Bind b
u
THeads
Flat Appl
TApp (lifts (S O) O ts) (lift (S O) O t)
t0
u2
end of h1
(h2)
by (lifts_tapp . . . .)
eq
TList
lifts (S O) O (TApp ts t)
TApp (lifts (S O) O ts) (lift (S O) O t)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
pr3
c
THead
Bind b
u
THeads (Flat Appl) (lifts (S O) O (TApp ts t)) t0
u2
we proved
∀c:C
.∀u2:T
.pr3 c (THeads (Flat Appl) (TApp ts t) (THead (Bind b) u t0)) u2
→(iso (THeads (Flat Appl) (TApp ts t) (THead (Bind b) u t0)) u2
→∀P:Prop.P
→(pr3
c
THead
Bind b
u
THeads (Flat Appl) (lifts (S O) O (TApp ts t)) t0
u2))
that is equivalent to
let u1 := THeads (Flat Appl) (TApp ts t) (THead (Bind b) u t0)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→(pr3
c
THead
Bind b
u
THeads (Flat Appl) (lifts (S O) O (TApp ts t)) t0
u2))
we proved
∀u:T
.∀t0:T
.∀c:C
.∀u2:T
.pr3 c (THeads (Flat Appl) ts (THead (Bind b) u t0)) u2
→(iso (THeads (Flat Appl) ts (THead (Bind b) u t0)) u2
→∀P:Prop.P
→(pr3
c
THead (Bind b) u (THeads (Flat Appl) (lifts (S O) O ts) t0)
u2))
→∀u:T
.∀t0:T
.let u1 := THeads (Flat Appl) (TApp ts t) (THead (Bind b) u t0)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→(pr3
c
THead
Bind b
u
THeads (Flat Appl) (lifts (S O) O (TApp ts t)) t0
u2))
that is equivalent to
∀u:T
.∀t0:T
.let u1 := THeads (Flat Appl) ts (THead (Bind b) u t0)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→(pr3
c
THead (Bind b) u (THeads (Flat Appl) (lifts (S O) O ts) t0)
u2))
→∀u:T
.∀t0:T
.let u1 := THeads (Flat Appl) (TApp ts t) (THead (Bind b) u t0)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→(pr3
c
THead
Bind b
u
THeads (Flat Appl) (lifts (S O) O (TApp ts t)) t0
u2))
∀ts:TList
.∀t:T
.∀u:T
.∀t0:T
.let u1 := THeads (Flat Appl) ts (THead (Bind b) u t0)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→(pr3
c
THead (Bind b) u (THeads (Flat Appl) (lifts (S O) O ts) t0)
u2))
→∀u:T
.∀t0:T
.let u1 := THeads (Flat Appl) (TApp ts t) (THead (Bind b) u t0)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→(pr3
c
THead
Bind b
u
THeads (Flat Appl) (lifts (S O) O (TApp ts t)) t0
u2))
end of h2
by (tlist_ind_rev . h1 h2 .)
we proved
∀u:T
.∀t0:T
.let u1 := THeads (Flat Appl) vs (THead (Bind b) u t0)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→(pr3
c
THead (Bind b) u (THeads (Flat Appl) (lifts (S O) O vs) t0)
u2))
we proved
∀b:B
.not (eq B b Abst)
→∀vs:TList
.∀u:T
.∀t0:T
.let u1 := THeads (Flat Appl) vs (THead (Bind b) u t0)
in ∀c:C
.∀u2:T
.pr3 c u1 u2
→((iso u1 u2)→∀P:Prop.P
→(pr3
c
THead (Bind b) u (THeads (Flat Appl) (lifts (S O) O vs) t0)
u2))