DEFINITION sc3_cast()
TYPE =
∀g:G
.∀a:A
.∀vs:TList
.∀c:C
.∀u:T
.sc3 g (asucc g a) c (THeads (Flat Appl) vs u)
→∀t:T
.sc3 g a c (THeads (Flat Appl) vs t)
→sc3 g a c (THeads (Flat Appl) vs (THead (Flat Cast) u t))
BODY =
assume g: G
assume a: A
we proceed by induction on a to prove
∀vs:TList
.∀c:C
.∀u:T
.sc3 g (asucc g a) c (THeads (Flat Appl) vs u)
→∀t:T
.sc3 g a c (THeads (Flat Appl) vs t)
→sc3 g a c (THeads (Flat Appl) vs (THead (Flat Cast) u t))
case ASort : n:nat n0:nat ⇒
the thesis becomes
∀vs:TList
.∀c:C
.∀u:T
.sc3 g (asucc g (ASort n n0)) c (THeads (Flat Appl) vs u)
→∀t:T
.sc3 g (ASort n n0) c (THeads (Flat Appl) vs t)
→(sc3
g
ASort n n0
c
THeads (Flat Appl) vs (THead (Flat Cast) u t))
assume vs: TList
assume c: C
assume u: T
we must prove
sc3 g (asucc g (ASort n n0)) c (THeads (Flat Appl) vs u)
→∀t:T
.sc3 g (ASort n n0) c (THeads (Flat Appl) vs t)
→(sc3
g
ASort n n0
c
THeads (Flat Appl) vs (THead (Flat Cast) u t))
or equivalently
(sc3
g
<λn1:nat.A> CASE n OF O⇒ASort O (next g n0) | S h⇒ASort h n0
c
THeads (Flat Appl) vs u)
→∀t:T
.sc3 g (ASort n n0) c (THeads (Flat Appl) vs t)
→(sc3
g
ASort n n0
c
THeads (Flat Appl) vs (THead (Flat Cast) u t))
suppose H:
sc3
g
<λn1:nat.A> CASE n OF O⇒ASort O (next g n0) | S h⇒ASort h n0
c
THeads (Flat Appl) vs u
assume t: T
we must prove
sc3 g (ASort n n0) c (THeads (Flat Appl) vs t)
→(sc3
g
ASort n n0
c
THeads (Flat Appl) vs (THead (Flat Cast) u t))
or equivalently
(land
arity g c (THeads (Flat Appl) vs t) (ASort n n0)
sn3 c (THeads (Flat Appl) vs t))
→(sc3
g
ASort n n0
c
THeads (Flat Appl) vs (THead (Flat Cast) u t))
suppose H0:
land
arity g c (THeads (Flat Appl) vs t) (ASort n n0)
sn3 c (THeads (Flat Appl) vs t)
we must prove
(sc3
g
<λn2:nat.A> CASE O OF O⇒ASort O (next g n0) | S h⇒ASort h n0
c
THeads (Flat Appl) vs u)
→((land
arity g c (THeads (Flat Appl) vs t) (ASort O n0)
sn3 c (THeads (Flat Appl) vs t))
→(land
arity
g
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
ASort O n0
sn3 c (THeads (Flat Appl) vs (THead (Flat Cast) u t))))
or equivalently
sc3 g (ASort O (next g n0)) c (THeads (Flat Appl) vs u)
→((land
arity g c (THeads (Flat Appl) vs t) (ASort O n0)
sn3 c (THeads (Flat Appl) vs t))
→(land
arity
g
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
ASort O n0
sn3 c (THeads (Flat Appl) vs (THead (Flat Cast) u t))))
suppose H1: sc3 g (ASort O (next g n0)) c (THeads (Flat Appl) vs u)
suppose H2:
land
arity g c (THeads (Flat Appl) vs t) (ASort O n0)
sn3 c (THeads (Flat Appl) vs t)
(H3) consider H1
consider H3
we proved sc3 g (ASort O (next g n0)) c (THeads (Flat Appl) vs u)
that is equivalent to
land
arity g c (THeads (Flat Appl) vs u) (ASort O (next g n0))
sn3 c (THeads (Flat Appl) vs u)
we proceed by induction on the previous result to prove
land
arity
g
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
ASort O n0
sn3 c (THeads (Flat Appl) vs (THead (Flat Cast) u t))
case conj : H4:arity g c (THeads (Flat Appl) vs u) (ASort O (next g n0)) H5:sn3 c (THeads (Flat Appl) vs u) ⇒
the thesis becomes
land
arity
g
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
ASort O n0
sn3 c (THeads (Flat Appl) vs (THead (Flat Cast) u t))
(H6) consider H2
we proceed by induction on H6 to prove
land
arity
g
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
ASort O n0
sn3 c (THeads (Flat Appl) vs (THead (Flat Cast) u t))
case conj : H7:arity g c (THeads (Flat Appl) vs t) (ASort O n0) H8:sn3 c (THeads (Flat Appl) vs t) ⇒
the thesis becomes
land
arity
g
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
ASort O n0
sn3 c (THeads (Flat Appl) vs (THead (Flat Cast) u t))
(h1)
consider H4
we proved arity g c (THeads (Flat Appl) vs u) (ASort O (next g n0))
that is equivalent to arity g c (THeads (Flat Appl) vs u) (asucc g (ASort O n0))
by (arity_appls_cast . . . . . . previous H7)
arity
g
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
ASort O n0
end of h1
(h2)
by (sn3_appls_cast . . . H5 . H8)
sn3 c (THeads (Flat Appl) vs (THead (Flat Cast) u t))
end of h2
by (conj . . h1 h2)
land
arity
g
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
ASort O n0
sn3 c (THeads (Flat Appl) vs (THead (Flat Cast) u t))
land
arity
g
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
ASort O n0
sn3 c (THeads (Flat Appl) vs (THead (Flat Cast) u t))
we proved
land
arity
g
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
ASort O n0
sn3 c (THeads (Flat Appl) vs (THead (Flat Cast) u t))
we proved
sc3 g (ASort O (next g n0)) c (THeads (Flat Appl) vs u)
→((land
arity g c (THeads (Flat Appl) vs t) (ASort O n0)
sn3 c (THeads (Flat Appl) vs t))
→(land
arity
g
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
ASort O n0
sn3 c (THeads (Flat Appl) vs (THead (Flat Cast) u t))))
(sc3
g
<λn2:nat.A> CASE O OF O⇒ASort O (next g n0) | S h⇒ASort h n0
c
THeads (Flat Appl) vs u)
→((land
arity g c (THeads (Flat Appl) vs t) (ASort O n0)
sn3 c (THeads (Flat Appl) vs t))
→(land
arity
g
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
ASort O n0
sn3 c (THeads (Flat Appl) vs (THead (Flat Cast) u t))))
assume n1: nat
suppose :
(sc3
g
<λn2:nat.A> CASE n1 OF O⇒ASort O (next g n0) | S h⇒ASort h n0
c
THeads (Flat Appl) vs u)
→((land
arity g c (THeads (Flat Appl) vs t) (ASort n1 n0)
sn3 c (THeads (Flat Appl) vs t))
→(land
arity
g
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
ASort n1 n0
sn3 c (THeads (Flat Appl) vs (THead (Flat Cast) u t))))
we must prove
(sc3
g
<λn2:nat.A> CASE S n1 OF O⇒ASort O (next g n0) | S h⇒ASort h n0
c
THeads (Flat Appl) vs u)
→((land
arity g c (THeads (Flat Appl) vs t) (ASort (S n1) n0)
sn3 c (THeads (Flat Appl) vs t))
→(land
arity
g
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
ASort (S n1) n0
sn3 c (THeads (Flat Appl) vs (THead (Flat Cast) u t))))
or equivalently
sc3 g (ASort n1 n0) c (THeads (Flat Appl) vs u)
→((land
arity g c (THeads (Flat Appl) vs t) (ASort (S n1) n0)
sn3 c (THeads (Flat Appl) vs t))
→(land
arity
g
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
ASort (S n1) n0
sn3 c (THeads (Flat Appl) vs (THead (Flat Cast) u t))))
suppose H1: sc3 g (ASort n1 n0) c (THeads (Flat Appl) vs u)
suppose H2:
land
arity g c (THeads (Flat Appl) vs t) (ASort (S n1) n0)
sn3 c (THeads (Flat Appl) vs t)
(H3) consider H1
consider H3
we proved sc3 g (ASort n1 n0) c (THeads (Flat Appl) vs u)
that is equivalent to
land
arity g c (THeads (Flat Appl) vs u) (ASort n1 n0)
sn3 c (THeads (Flat Appl) vs u)
we proceed by induction on the previous result to prove
land
arity
g
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
ASort (S n1) n0
sn3 c (THeads (Flat Appl) vs (THead (Flat Cast) u t))
case conj : H4:arity g c (THeads (Flat Appl) vs u) (ASort n1 n0) H5:sn3 c (THeads (Flat Appl) vs u) ⇒
the thesis becomes
land
arity
g
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
ASort (S n1) n0
sn3 c (THeads (Flat Appl) vs (THead (Flat Cast) u t))
(H6) consider H2
we proceed by induction on H6 to prove
land
arity
g
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
ASort (S n1) n0
sn3 c (THeads (Flat Appl) vs (THead (Flat Cast) u t))
case conj : H7:arity g c (THeads (Flat Appl) vs t) (ASort (S n1) n0) H8:sn3 c (THeads (Flat Appl) vs t) ⇒
the thesis becomes
land
arity
g
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
ASort (S n1) n0
sn3 c (THeads (Flat Appl) vs (THead (Flat Cast) u t))
(h1)
consider H4
we proved arity g c (THeads (Flat Appl) vs u) (ASort n1 n0)
that is equivalent to arity g c (THeads (Flat Appl) vs u) (asucc g (ASort (S n1) n0))
by (arity_appls_cast . . . . . . previous H7)
arity
g
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
ASort (S n1) n0
end of h1
(h2)
by (sn3_appls_cast . . . H5 . H8)
sn3 c (THeads (Flat Appl) vs (THead (Flat Cast) u t))
end of h2
by (conj . . h1 h2)
land
arity
g
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
ASort (S n1) n0
sn3 c (THeads (Flat Appl) vs (THead (Flat Cast) u t))
land
arity
g
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
ASort (S n1) n0
sn3 c (THeads (Flat Appl) vs (THead (Flat Cast) u t))
we proved
land
arity
g
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
ASort (S n1) n0
sn3 c (THeads (Flat Appl) vs (THead (Flat Cast) u t))
we proved
sc3 g (ASort n1 n0) c (THeads (Flat Appl) vs u)
→((land
arity g c (THeads (Flat Appl) vs t) (ASort (S n1) n0)
sn3 c (THeads (Flat Appl) vs t))
→(land
arity
g
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
ASort (S n1) n0
sn3 c (THeads (Flat Appl) vs (THead (Flat Cast) u t))))
(sc3
g
<λn2:nat.A> CASE S n1 OF O⇒ASort O (next g n0) | S h⇒ASort h n0
c
THeads (Flat Appl) vs u)
→((land
arity g c (THeads (Flat Appl) vs t) (ASort (S n1) n0)
sn3 c (THeads (Flat Appl) vs t))
→(land
arity
g
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
ASort (S n1) n0
sn3 c (THeads (Flat Appl) vs (THead (Flat Cast) u t))))
by (previous . H H0)
we proved
land
arity
g
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
ASort n n0
sn3 c (THeads (Flat Appl) vs (THead (Flat Cast) u t))
that is equivalent to
sc3
g
ASort n n0
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
we proved
(land
arity g c (THeads (Flat Appl) vs t) (ASort n n0)
sn3 c (THeads (Flat Appl) vs t))
→(sc3
g
ASort n n0
c
THeads (Flat Appl) vs (THead (Flat Cast) u t))
that is equivalent to
sc3 g (ASort n n0) c (THeads (Flat Appl) vs t)
→(sc3
g
ASort n n0
c
THeads (Flat Appl) vs (THead (Flat Cast) u t))
we proved
(sc3
g
<λn1:nat.A> CASE n OF O⇒ASort O (next g n0) | S h⇒ASort h n0
c
THeads (Flat Appl) vs u)
→∀t:T
.sc3 g (ASort n n0) c (THeads (Flat Appl) vs t)
→(sc3
g
ASort n n0
c
THeads (Flat Appl) vs (THead (Flat Cast) u t))
that is equivalent to
sc3 g (asucc g (ASort n n0)) c (THeads (Flat Appl) vs u)
→∀t:T
.sc3 g (ASort n n0) c (THeads (Flat Appl) vs t)
→(sc3
g
ASort n n0
c
THeads (Flat Appl) vs (THead (Flat Cast) u t))
∀vs:TList
.∀c:C
.∀u:T
.sc3 g (asucc g (ASort n n0)) c (THeads (Flat Appl) vs u)
→∀t:T
.sc3 g (ASort n n0) c (THeads (Flat Appl) vs t)
→(sc3
g
ASort n n0
c
THeads (Flat Appl) vs (THead (Flat Cast) u t))
case AHead : a0:A a1:A ⇒
the thesis becomes
∀vs:TList
.∀c:C
.∀u:T
.sc3 g (asucc g (AHead a0 a1)) c (THeads (Flat Appl) vs u)
→∀t:T
.sc3 g (AHead a0 a1) c (THeads (Flat Appl) vs t)
→(sc3
g
AHead a0 a1
c
THeads (Flat Appl) vs (THead (Flat Cast) u t))
() by induction hypothesis we know
∀vs:TList
.∀c:C
.∀u:T
.sc3 g (asucc g a0) c (THeads (Flat Appl) vs u)
→∀t:T
.sc3 g a0 c (THeads (Flat Appl) vs t)
→sc3 g a0 c (THeads (Flat Appl) vs (THead (Flat Cast) u t))
(H0) by induction hypothesis we know
∀vs:TList
.∀c:C
.∀u:T
.sc3 g (asucc g a1) c (THeads (Flat Appl) vs u)
→∀t:T
.sc3 g a1 c (THeads (Flat Appl) vs t)
→sc3 g a1 c (THeads (Flat Appl) vs (THead (Flat Cast) u t))
assume vs: TList
assume c: C
assume u: T
we must prove
sc3 g (asucc g (AHead a0 a1)) c (THeads (Flat Appl) vs u)
→∀t:T
.sc3 g (AHead a0 a1) c (THeads (Flat Appl) vs t)
→(sc3
g
AHead a0 a1
c
THeads (Flat Appl) vs (THead (Flat Cast) u t))
or equivalently
(land
arity g c (THeads (Flat Appl) vs u) (AHead a0 (asucc g a1))
∀d:C
.∀w:T
.sc3 g a0 d w
→∀is:PList
.drop1 is d c
→(sc3
g
asucc g a1
d
THead (Flat Appl) w (lift1 is (THeads (Flat Appl) vs u))))
→∀t:T
.sc3 g (AHead a0 a1) c (THeads (Flat Appl) vs t)
→(sc3
g
AHead a0 a1
c
THeads (Flat Appl) vs (THead (Flat Cast) u t))
suppose H1:
land
arity g c (THeads (Flat Appl) vs u) (AHead a0 (asucc g a1))
∀d:C
.∀w:T
.sc3 g a0 d w
→∀is:PList
.drop1 is d c
→(sc3
g
asucc g a1
d
THead (Flat Appl) w (lift1 is (THeads (Flat Appl) vs u)))
assume t: T
we must prove
sc3 g (AHead a0 a1) c (THeads (Flat Appl) vs t)
→(sc3
g
AHead a0 a1
c
THeads (Flat Appl) vs (THead (Flat Cast) u t))
or equivalently
(land
arity g c (THeads (Flat Appl) vs t) (AHead a0 a1)
∀d:C
.∀w:T
.sc3 g a0 d w
→∀is:PList
.drop1 is d c
→sc3 g a1 d (THead (Flat Appl) w (lift1 is (THeads (Flat Appl) vs t))))
→(sc3
g
AHead a0 a1
c
THeads (Flat Appl) vs (THead (Flat Cast) u t))
suppose H2:
land
arity g c (THeads (Flat Appl) vs t) (AHead a0 a1)
∀d:C
.∀w:T
.sc3 g a0 d w
→∀is:PList
.drop1 is d c
→sc3 g a1 d (THead (Flat Appl) w (lift1 is (THeads (Flat Appl) vs t)))
(H3) consider H1
we proceed by induction on H3 to prove
land
arity
g
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
AHead a0 a1
∀d:C
.∀w:T
.sc3 g a0 d w
→∀is:PList
.drop1 is d c
→(sc3
g
a1
d
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (THead (Flat Cast) u t)))
case conj : H4:arity g c (THeads (Flat Appl) vs u) (AHead a0 (asucc g a1)) H5:∀d:C.∀w:T.(sc3 g a0 d w)→∀is:PList.(drop1 is d c)→(sc3 g (asucc g a1) d (THead (Flat Appl) w (lift1 is (THeads (Flat Appl) vs u)))) ⇒
the thesis becomes
land
arity
g
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
AHead a0 a1
∀d:C
.∀w:T
.sc3 g a0 d w
→∀is:PList
.drop1 is d c
→(sc3
g
a1
d
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (THead (Flat Cast) u t)))
(H6) consider H2
we proceed by induction on H6 to prove
land
arity
g
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
AHead a0 a1
∀d:C
.∀w:T
.sc3 g a0 d w
→∀is:PList
.drop1 is d c
→(sc3
g
a1
d
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (THead (Flat Cast) u t)))
case conj : H7:arity g c (THeads (Flat Appl) vs t) (AHead a0 a1) H8:∀d:C.∀w:T.(sc3 g a0 d w)→∀is:PList.(drop1 is d c)→(sc3 g a1 d (THead (Flat Appl) w (lift1 is (THeads (Flat Appl) vs t)))) ⇒
the thesis becomes
land
arity
g
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
AHead a0 a1
∀d:C
.∀w:T
.sc3 g a0 d w
→∀is:PList
.drop1 is d c
→(sc3
g
a1
d
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (THead (Flat Cast) u t)))
(h1)
consider H4
we proved arity g c (THeads (Flat Appl) vs u) (AHead a0 (asucc g a1))
that is equivalent to arity g c (THeads (Flat Appl) vs u) (asucc g (AHead a0 a1))
by (arity_appls_cast . . . . . . previous H7)
arity
g
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
AHead a0 a1
end of h1
(h2)
assume d: C
assume w: T
suppose H9: sc3 g a0 d w
assume is: PList
suppose H10: drop1 is d c
(H_y)
by (H0 .)
∀c:C
.∀u:T
.sc3 g (asucc g a1) c (THeads (Flat Appl) (TCons w (lifts1 is vs)) u)
→∀t:T
.sc3 g a1 c (THeads (Flat Appl) (TCons w (lifts1 is vs)) t)
→(sc3
g
a1
c
THeads
Flat Appl
TCons w (lifts1 is vs)
THead (Flat Cast) u t)
end of H_y
(h1)
(h1)
(h1)
by (lifts1_flat . . . .)
we proved
eq
T
lift1 is (THeads (Flat Appl) vs u)
THeads (Flat Appl) (lifts1 is vs) (lift1 is u)
we proceed by induction on the previous result to prove
sc3
g
asucc g a1
d
THead (Flat Appl) w (THeads (Flat Appl) (lifts1 is vs) (lift1 is u))
case refl_equal : ⇒
the thesis becomes
sc3
g
asucc g a1
d
THead (Flat Appl) w (lift1 is (THeads (Flat Appl) vs u))
by (H5 . . H9 . H10)
sc3
g
asucc g a1
d
THead (Flat Appl) w (lift1 is (THeads (Flat Appl) vs u))
we proved
sc3
g
asucc g a1
d
THead (Flat Appl) w (THeads (Flat Appl) (lifts1 is vs) (lift1 is u))
sc3
g
asucc g a1
d
THeads (Flat Appl) (TCons w (lifts1 is vs)) (lift1 is u)
end of h1
(h2)
by (lifts1_flat . . . .)
we proved
eq
T
lift1 is (THeads (Flat Appl) vs t)
THeads (Flat Appl) (lifts1 is vs) (lift1 is t)
we proceed by induction on the previous result to prove
sc3
g
a1
d
THead (Flat Appl) w (THeads (Flat Appl) (lifts1 is vs) (lift1 is t))
case refl_equal : ⇒
the thesis becomes sc3 g a1 d (THead (Flat Appl) w (lift1 is (THeads (Flat Appl) vs t)))
by (H8 . . H9 . H10)
sc3 g a1 d (THead (Flat Appl) w (lift1 is (THeads (Flat Appl) vs t)))
we proved
sc3
g
a1
d
THead (Flat Appl) w (THeads (Flat Appl) (lifts1 is vs) (lift1 is t))
sc3 g a1 d (THeads (Flat Appl) (TCons w (lifts1 is vs)) (lift1 is t))
end of h2
by (H_y . . h1 . h2)
we proved
sc3
g
a1
d
THeads
Flat Appl
TCons w (lifts1 is vs)
THead (Flat Cast) (lift1 is u) (lift1 is t)
sc3
g
a1
d
THead
Flat Appl
w
THeads
Flat Appl
lifts1 is vs
THead (Flat Cast) (lift1 is u) (lift1 is t)
end of h1
(h2)
by (lift1_flat . . . .)
eq
T
lift1 is (THead (Flat Cast) u t)
THead (Flat Cast) (lift1 is u) (lift1 is t)
end of h2
by (eq_ind_r . . . h1 . h2)
sc3
g
a1
d
THead
Flat Appl
w
THeads (Flat Appl) (lifts1 is vs) (lift1 is (THead (Flat Cast) u t))
end of h1
(h2)
by (lifts1_flat . . . .)
eq
T
lift1 is (THeads (Flat Appl) vs (THead (Flat Cast) u t))
THeads (Flat Appl) (lifts1 is vs) (lift1 is (THead (Flat Cast) u t))
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
sc3
g
a1
d
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (THead (Flat Cast) u t))
∀d:C
.∀w:T
.sc3 g a0 d w
→∀is:PList
.drop1 is d c
→(sc3
g
a1
d
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (THead (Flat Cast) u t)))
end of h2
by (conj . . h1 h2)
land
arity
g
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
AHead a0 a1
∀d:C
.∀w:T
.sc3 g a0 d w
→∀is:PList
.drop1 is d c
→(sc3
g
a1
d
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (THead (Flat Cast) u t)))
land
arity
g
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
AHead a0 a1
∀d:C
.∀w:T
.sc3 g a0 d w
→∀is:PList
.drop1 is d c
→(sc3
g
a1
d
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (THead (Flat Cast) u t)))
we proved
land
arity
g
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
AHead a0 a1
∀d:C
.∀w:T
.sc3 g a0 d w
→∀is:PList
.drop1 is d c
→(sc3
g
a1
d
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (THead (Flat Cast) u t)))
that is equivalent to
sc3
g
AHead a0 a1
c
THeads (Flat Appl) vs (THead (Flat Cast) u t)
we proved
(land
arity g c (THeads (Flat Appl) vs t) (AHead a0 a1)
∀d:C
.∀w:T
.sc3 g a0 d w
→∀is:PList
.drop1 is d c
→sc3 g a1 d (THead (Flat Appl) w (lift1 is (THeads (Flat Appl) vs t))))
→(sc3
g
AHead a0 a1
c
THeads (Flat Appl) vs (THead (Flat Cast) u t))
that is equivalent to
sc3 g (AHead a0 a1) c (THeads (Flat Appl) vs t)
→(sc3
g
AHead a0 a1
c
THeads (Flat Appl) vs (THead (Flat Cast) u t))
we proved
(land
arity g c (THeads (Flat Appl) vs u) (AHead a0 (asucc g a1))
∀d:C
.∀w:T
.sc3 g a0 d w
→∀is:PList
.drop1 is d c
→(sc3
g
asucc g a1
d
THead (Flat Appl) w (lift1 is (THeads (Flat Appl) vs u))))
→∀t:T
.sc3 g (AHead a0 a1) c (THeads (Flat Appl) vs t)
→(sc3
g
AHead a0 a1
c
THeads (Flat Appl) vs (THead (Flat Cast) u t))
that is equivalent to
sc3 g (asucc g (AHead a0 a1)) c (THeads (Flat Appl) vs u)
→∀t:T
.sc3 g (AHead a0 a1) c (THeads (Flat Appl) vs t)
→(sc3
g
AHead a0 a1
c
THeads (Flat Appl) vs (THead (Flat Cast) u t))
∀vs:TList
.∀c:C
.∀u:T
.sc3 g (asucc g (AHead a0 a1)) c (THeads (Flat Appl) vs u)
→∀t:T
.sc3 g (AHead a0 a1) c (THeads (Flat Appl) vs t)
→(sc3
g
AHead a0 a1
c
THeads (Flat Appl) vs (THead (Flat Cast) u t))
we proved
∀vs:TList
.∀c:C
.∀u:T
.sc3 g (asucc g a) c (THeads (Flat Appl) vs u)
→∀t:T
.sc3 g a c (THeads (Flat Appl) vs t)
→sc3 g a c (THeads (Flat Appl) vs (THead (Flat Cast) u t))
we proved
∀g:G
.∀a:A
.∀vs:TList
.∀c:C
.∀u:T
.sc3 g (asucc g a) c (THeads (Flat Appl) vs u)
→∀t:T
.sc3 g a c (THeads (Flat Appl) vs t)
→sc3 g a c (THeads (Flat Appl) vs (THead (Flat Cast) u t))