DEFINITION sc3_bind()
TYPE =
∀g:G
.∀b:B
.not (eq B b Abst)
→∀a1:A
.∀a2:A
.∀vs:TList
.∀c:C
.∀v:T
.∀t:T
.(sc3
g
a2
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O vs) t)
→(sc3 g a1 c v
→sc3 g a2 c (THeads (Flat Appl) vs (THead (Bind b) v t)))
BODY =
assume g: G
assume b: B
suppose H: not (eq B b Abst)
assume a1: A
assume a2: A
we proceed by induction on a2 to prove
∀vs:TList
.∀c:C
.∀v:T
.∀t:T
.(sc3
g
a2
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O vs) t)
→(sc3 g a1 c v
→sc3 g a2 c (THeads (Flat Appl) vs (THead (Bind b) v t)))
case ASort : n:nat n0:nat ⇒
the thesis becomes
∀vs:TList
.∀c:C
.∀v:T
.∀t:T
.(sc3
g
ASort n n0
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O vs) t)
→(sc3 g a1 c v
→sc3 g (ASort n n0) c (THeads (Flat Appl) vs (THead (Bind b) v t)))
assume vs: TList
assume c: C
assume v: T
assume t: T
we must prove
(sc3
g
ASort n n0
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O vs) t)
→(sc3 g a1 c v
→sc3 g (ASort n n0) c (THeads (Flat Appl) vs (THead (Bind b) v t)))
or equivalently
(land
arity
g
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O vs) t
ASort n n0
sn3
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O vs) t)
→(sc3 g a1 c v
→sc3 g (ASort n n0) c (THeads (Flat Appl) vs (THead (Bind b) v t)))
suppose H0:
land
arity
g
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O vs) t
ASort n n0
sn3
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O vs) t
suppose H1: sc3 g a1 c v
(H2) consider H0
we proceed by induction on H2 to prove
land
arity
g
c
THeads (Flat Appl) vs (THead (Bind b) v t)
ASort n n0
sn3 c (THeads (Flat Appl) vs (THead (Bind b) v t))
case conj : H3:arity g (CHead c (Bind b) v) (THeads (Flat Appl) (lifts (S O) O vs) t) (ASort n n0) H4:sn3 (CHead c (Bind b) v) (THeads (Flat Appl) (lifts (S O) O vs) t) ⇒
the thesis becomes
land
arity
g
c
THeads (Flat Appl) vs (THead (Bind b) v t)
ASort n n0
sn3 c (THeads (Flat Appl) vs (THead (Bind b) v t))
(h1)
by (sc3_arity_gen . . . . H1)
we proved arity g c v a1
by (arity_appls_bind . . H . . . previous . . . H3)
arity
g
c
THeads (Flat Appl) vs (THead (Bind b) v t)
ASort n n0
end of h1
(h2)
by (sc3_sn3 . . . . H1)
we proved sn3 c v
by (sn3_appls_bind . H . . previous . . H4)
sn3 c (THeads (Flat Appl) vs (THead (Bind b) v t))
end of h2
by (conj . . h1 h2)
land
arity
g
c
THeads (Flat Appl) vs (THead (Bind b) v t)
ASort n n0
sn3 c (THeads (Flat Appl) vs (THead (Bind b) v t))
we proved
land
arity
g
c
THeads (Flat Appl) vs (THead (Bind b) v t)
ASort n n0
sn3 c (THeads (Flat Appl) vs (THead (Bind b) v t))
that is equivalent to sc3 g (ASort n n0) c (THeads (Flat Appl) vs (THead (Bind b) v t))
we proved
(land
arity
g
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O vs) t
ASort n n0
sn3
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O vs) t)
→(sc3 g a1 c v
→sc3 g (ASort n n0) c (THeads (Flat Appl) vs (THead (Bind b) v t)))
that is equivalent to
(sc3
g
ASort n n0
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O vs) t)
→(sc3 g a1 c v
→sc3 g (ASort n n0) c (THeads (Flat Appl) vs (THead (Bind b) v t)))
∀vs:TList
.∀c:C
.∀v:T
.∀t:T
.(sc3
g
ASort n n0
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O vs) t)
→(sc3 g a1 c v
→sc3 g (ASort n n0) c (THeads (Flat Appl) vs (THead (Bind b) v t)))
case AHead : a:A a0:A ⇒
the thesis becomes
∀vs:TList
.∀c:C
.∀v:T
.∀t:T
.(sc3
g
AHead a a0
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O vs) t)
→(sc3 g a1 c v
→sc3 g (AHead a a0) c (THeads (Flat Appl) vs (THead (Bind b) v t)))
() by induction hypothesis we know
∀vs:TList
.∀c:C
.∀v:T
.∀t:T
.(sc3
g
a
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O vs) t)
→(sc3 g a1 c v
→sc3 g a c (THeads (Flat Appl) vs (THead (Bind b) v t)))
(H1) by induction hypothesis we know
∀vs:TList
.∀c:C
.∀v:T
.∀t:T
.(sc3
g
a0
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O vs) t)
→(sc3 g a1 c v
→sc3 g a0 c (THeads (Flat Appl) vs (THead (Bind b) v t)))
assume vs: TList
assume c: C
assume v: T
assume t: T
we must prove
(sc3
g
AHead a a0
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O vs) t)
→(sc3 g a1 c v
→sc3 g (AHead a a0) c (THeads (Flat Appl) vs (THead (Bind b) v t)))
or equivalently
(land
arity
g
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O vs) t
AHead a a0
∀d:C
.∀w:T
.sc3 g a d w
→∀is:PList
.drop1 is d (CHead c (Bind b) v)
→(sc3
g
a0
d
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) (lifts (S O) O vs) t)))
→(sc3 g a1 c v
→sc3 g (AHead a a0) c (THeads (Flat Appl) vs (THead (Bind b) v t)))
suppose H2:
land
arity
g
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O vs) t
AHead a a0
∀d:C
.∀w:T
.sc3 g a d w
→∀is:PList
.drop1 is d (CHead c (Bind b) v)
→(sc3
g
a0
d
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) (lifts (S O) O vs) t))
suppose H3: sc3 g a1 c v
(H4) consider H2
we proceed by induction on H4 to prove
land
arity
g
c
THeads (Flat Appl) vs (THead (Bind b) v t)
AHead a a0
∀d:C
.∀w:T
.sc3 g a d w
→∀is:PList
.drop1 is d c
→(sc3
g
a0
d
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (THead (Bind b) v t)))
case conj : H5:arity g (CHead c (Bind b) v) (THeads (Flat Appl) (lifts (S O) O vs) t) (AHead a a0) H6:∀d:C.∀w:T.(sc3 g a d w)→∀is:PList.(drop1 is d (CHead c (Bind b) v))→(sc3 g a0 d (THead (Flat Appl) w (lift1 is (THeads (Flat Appl) (lifts (S O) O vs) t)))) ⇒
the thesis becomes
land
arity
g
c
THeads (Flat Appl) vs (THead (Bind b) v t)
AHead a a0
∀d:C
.∀w:T
.sc3 g a d w
→∀is:PList
.drop1 is d c
→(sc3
g
a0
d
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (THead (Bind b) v t)))
(h1)
by (sc3_arity_gen . . . . H3)
we proved arity g c v a1
by (arity_appls_bind . . H . . . previous . . . H5)
arity
g
c
THeads (Flat Appl) vs (THead (Bind b) v t)
AHead a a0
end of h1
(h2)
assume d: C
assume w: T
suppose H7: sc3 g a d w
assume is: PList
suppose H8: drop1 is d c
(H_y)
by (H1 .)
∀c:C
.∀v:T
.∀t:T
.(sc3
g
a0
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O (TCons w (lifts1 is vs))) t)
→(sc3 g a1 c v
→(sc3
g
a0
c
THeads (Flat Appl) (TCons w (lifts1 is vs)) (THead (Bind b) v t)))
end of H_y
(h1)
(h1)
(h1)
by (lifts1_xhg . .)
we proved
eq
TList
lifts1 (Ss is) (lifts (S O) O vs)
lifts (S O) O (lifts1 is vs)
we proceed by induction on the previous result to prove
sc3
g
a0
CHead d (Bind b) (lift1 is v)
THead
Flat Appl
lift (S O) O w
THeads (Flat Appl) (lifts (S O) O (lifts1 is vs)) (lift1 (Ss is) t)
case refl_equal : ⇒
the thesis becomes
sc3
g
a0
CHead d (Bind b) (lift1 is v)
THead
Flat Appl
lift (S O) O w
THeads
Flat Appl
lifts1 (Ss is) (lifts (S O) O vs)
lift1 (Ss is) t
by (lifts1_flat . . . .)
we proved
eq
T
lift1 (Ss is) (THeads (Flat Appl) (lifts (S O) O vs) t)
THeads
Flat Appl
lifts1 (Ss is) (lifts (S O) O vs)
lift1 (Ss is) t
we proceed by induction on the previous result to prove
sc3
g
a0
CHead d (Bind b) (lift1 is v)
THead
Flat Appl
lift (S O) O w
THeads
Flat Appl
lifts1 (Ss is) (lifts (S O) O vs)
lift1 (Ss is) t
case refl_equal : ⇒
the thesis becomes
sc3
g
a0
CHead d (Bind b) (lift1 is v)
THead
Flat Appl
lift (S O) O w
lift1 (Ss is) (THeads (Flat Appl) (lifts (S O) O vs) t)
(h1)
by (drop_refl .)
we proved drop O O d d
that is equivalent to drop (r (Bind b) O) O d d
by (drop_drop . . . . previous .)
we proved drop (S O) O (CHead d (Bind b) (lift1 is v)) d
by (sc3_lift . . . . H7 . . . previous)
sc3 g a (CHead d (Bind b) (lift1 is v)) (lift (S O) O w)
end of h1
(h2)
by (drop1_skip_bind . . . . . H8)
drop1 (Ss is) (CHead d (Bind b) (lift1 is v)) (CHead c (Bind b) v)
end of h2
by (H6 . . h1 . h2)
sc3
g
a0
CHead d (Bind b) (lift1 is v)
THead
Flat Appl
lift (S O) O w
lift1 (Ss is) (THeads (Flat Appl) (lifts (S O) O vs) t)
sc3
g
a0
CHead d (Bind b) (lift1 is v)
THead
Flat Appl
lift (S O) O w
THeads
Flat Appl
lifts1 (Ss is) (lifts (S O) O vs)
lift1 (Ss is) t
we proved
sc3
g
a0
CHead d (Bind b) (lift1 is v)
THead
Flat Appl
lift (S O) O w
THeads (Flat Appl) (lifts (S O) O (lifts1 is vs)) (lift1 (Ss is) t)
sc3
g
a0
CHead d (Bind b) (lift1 is v)
THeads
Flat Appl
lifts (S O) O (TCons w (lifts1 is vs))
lift1 (Ss is) t
end of h1
(h2)
by (sc3_lift1 . . . . . . H3 H8)
sc3 g a1 d (lift1 is v)
end of h2
by (H_y . . . h1 h2)
we proved
sc3
g
a0
d
THeads
Flat Appl
TCons w (lifts1 is vs)
THead (Bind b) (lift1 is v) (lift1 (Ss is) t)
sc3
g
a0
d
THead
Flat Appl
w
THeads
Flat Appl
lifts1 is vs
THead (Bind b) (lift1 is v) (lift1 (Ss is) t)
end of h1
(h2)
by (lift1_bind . . . .)
eq
T
lift1 is (THead (Bind b) v t)
THead (Bind b) (lift1 is v) (lift1 (Ss is) t)
end of h2
by (eq_ind_r . . . h1 . h2)
sc3
g
a0
d
THead
Flat Appl
w
THeads (Flat Appl) (lifts1 is vs) (lift1 is (THead (Bind b) v t))
end of h1
(h2)
by (lifts1_flat . . . .)
eq
T
lift1 is (THeads (Flat Appl) vs (THead (Bind b) v t))
THeads (Flat Appl) (lifts1 is vs) (lift1 is (THead (Bind b) v t))
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
sc3
g
a0
d
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (THead (Bind b) v t))
∀d:C
.∀w:T
.sc3 g a d w
→∀is:PList
.drop1 is d c
→(sc3
g
a0
d
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (THead (Bind b) v t)))
end of h2
by (conj . . h1 h2)
land
arity
g
c
THeads (Flat Appl) vs (THead (Bind b) v t)
AHead a a0
∀d:C
.∀w:T
.sc3 g a d w
→∀is:PList
.drop1 is d c
→(sc3
g
a0
d
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (THead (Bind b) v t)))
we proved
land
arity
g
c
THeads (Flat Appl) vs (THead (Bind b) v t)
AHead a a0
∀d:C
.∀w:T
.sc3 g a d w
→∀is:PList
.drop1 is d c
→(sc3
g
a0
d
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (THead (Bind b) v t)))
that is equivalent to sc3 g (AHead a a0) c (THeads (Flat Appl) vs (THead (Bind b) v t))
we proved
(land
arity
g
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O vs) t
AHead a a0
∀d:C
.∀w:T
.sc3 g a d w
→∀is:PList
.drop1 is d (CHead c (Bind b) v)
→(sc3
g
a0
d
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) (lifts (S O) O vs) t)))
→(sc3 g a1 c v
→sc3 g (AHead a a0) c (THeads (Flat Appl) vs (THead (Bind b) v t)))
that is equivalent to
(sc3
g
AHead a a0
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O vs) t)
→(sc3 g a1 c v
→sc3 g (AHead a a0) c (THeads (Flat Appl) vs (THead (Bind b) v t)))
∀vs:TList
.∀c:C
.∀v:T
.∀t:T
.(sc3
g
AHead a a0
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O vs) t)
→(sc3 g a1 c v
→sc3 g (AHead a a0) c (THeads (Flat Appl) vs (THead (Bind b) v t)))
we proved
∀vs:TList
.∀c:C
.∀v:T
.∀t:T
.(sc3
g
a2
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O vs) t)
→(sc3 g a1 c v
→sc3 g a2 c (THeads (Flat Appl) vs (THead (Bind b) v t)))
we proved
∀g:G
.∀b:B
.not (eq B b Abst)
→∀a1:A
.∀a2:A
.∀vs:TList
.∀c:C
.∀v:T
.∀t:T
.(sc3
g
a2
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O vs) t)
→(sc3 g a1 c v
→sc3 g a2 c (THeads (Flat Appl) vs (THead (Bind b) v t)))