DEFINITION sc3_abbr()
TYPE =
∀g:G
.∀a:A
.∀vs:TList
.∀i:nat
.∀d:C
.∀v:T
.∀c:C
.sc3 g a c (THeads (Flat Appl) vs (lift (S i) O v))
→(getl i c (CHead d (Bind Abbr) v)
→sc3 g a c (THeads (Flat Appl) vs (TLRef i)))
BODY =
assume g: G
assume a: A
we proceed by induction on a to prove
∀vs:TList
.∀i:nat
.∀d:C
.∀v:T
.∀c:C
.sc3 g a c (THeads (Flat Appl) vs (lift (S i) O v))
→(getl i c (CHead d (Bind Abbr) v)
→sc3 g a c (THeads (Flat Appl) vs (TLRef i)))
case ASort : n:nat n0:nat ⇒
the thesis becomes
∀vs:TList
.∀i:nat
.∀d:C
.∀v:T
.∀c:C
.sc3 g (ASort n n0) c (THeads (Flat Appl) vs (lift (S i) O v))
→(getl i c (CHead d (Bind Abbr) v)
→sc3 g (ASort n n0) c (THeads (Flat Appl) vs (TLRef i)))
assume vs: TList
assume i: nat
assume d: C
assume v: T
assume c: C
we must prove
sc3 g (ASort n n0) c (THeads (Flat Appl) vs (lift (S i) O v))
→(getl i c (CHead d (Bind Abbr) v)
→sc3 g (ASort n n0) c (THeads (Flat Appl) vs (TLRef i)))
or equivalently
(land
arity g c (THeads (Flat Appl) vs (lift (S i) O v)) (ASort n n0)
sn3 c (THeads (Flat Appl) vs (lift (S i) O v)))
→(getl i c (CHead d (Bind Abbr) v)
→sc3 g (ASort n n0) c (THeads (Flat Appl) vs (TLRef i)))
suppose H:
land
arity g c (THeads (Flat Appl) vs (lift (S i) O v)) (ASort n n0)
sn3 c (THeads (Flat Appl) vs (lift (S i) O v))
suppose H0: getl i c (CHead d (Bind Abbr) v)
(H1) consider H
we proceed by induction on H1 to prove
land
arity g c (THeads (Flat Appl) vs (TLRef i)) (ASort n n0)
sn3 c (THeads (Flat Appl) vs (TLRef i))
case conj : H2:arity g c (THeads (Flat Appl) vs (lift (S i) O v)) (ASort n n0) H3:sn3 c (THeads (Flat Appl) vs (lift (S i) O v)) ⇒
the thesis becomes
land
arity g c (THeads (Flat Appl) vs (TLRef i)) (ASort n n0)
sn3 c (THeads (Flat Appl) vs (TLRef i))
(h1)
by (arity_appls_abbr . . . . . H0 . . H2)
arity g c (THeads (Flat Appl) vs (TLRef i)) (ASort n n0)
end of h1
(h2)
by (sn3_appls_abbr . . . . H0 . H3)
sn3 c (THeads (Flat Appl) vs (TLRef i))
end of h2
by (conj . . h1 h2)
land
arity g c (THeads (Flat Appl) vs (TLRef i)) (ASort n n0)
sn3 c (THeads (Flat Appl) vs (TLRef i))
we proved
land
arity g c (THeads (Flat Appl) vs (TLRef i)) (ASort n n0)
sn3 c (THeads (Flat Appl) vs (TLRef i))
that is equivalent to sc3 g (ASort n n0) c (THeads (Flat Appl) vs (TLRef i))
we proved
(land
arity g c (THeads (Flat Appl) vs (lift (S i) O v)) (ASort n n0)
sn3 c (THeads (Flat Appl) vs (lift (S i) O v)))
→(getl i c (CHead d (Bind Abbr) v)
→sc3 g (ASort n n0) c (THeads (Flat Appl) vs (TLRef i)))
that is equivalent to
sc3 g (ASort n n0) c (THeads (Flat Appl) vs (lift (S i) O v))
→(getl i c (CHead d (Bind Abbr) v)
→sc3 g (ASort n n0) c (THeads (Flat Appl) vs (TLRef i)))
∀vs:TList
.∀i:nat
.∀d:C
.∀v:T
.∀c:C
.sc3 g (ASort n n0) c (THeads (Flat Appl) vs (lift (S i) O v))
→(getl i c (CHead d (Bind Abbr) v)
→sc3 g (ASort n n0) c (THeads (Flat Appl) vs (TLRef i)))
case AHead : a0:A a1:A ⇒
the thesis becomes
∀vs:TList
.∀i:nat
.∀d:C
.∀v:T
.∀c:C
.sc3 g (AHead a0 a1) c (THeads (Flat Appl) vs (lift (S i) O v))
→(getl i c (CHead d (Bind Abbr) v)
→sc3 g (AHead a0 a1) c (THeads (Flat Appl) vs (TLRef i)))
() by induction hypothesis we know
∀vs:TList
.∀i:nat
.∀d:C
.∀v:T
.∀c:C
.sc3 g a0 c (THeads (Flat Appl) vs (lift (S i) O v))
→(getl i c (CHead d (Bind Abbr) v)
→sc3 g a0 c (THeads (Flat Appl) vs (TLRef i)))
(H0) by induction hypothesis we know
∀vs:TList
.∀i:nat
.∀d:C
.∀v:T
.∀c:C
.sc3 g a1 c (THeads (Flat Appl) vs (lift (S i) O v))
→(getl i c (CHead d (Bind Abbr) v)
→sc3 g a1 c (THeads (Flat Appl) vs (TLRef i)))
assume vs: TList
assume i: nat
assume d: C
assume v: T
assume c: C
we must prove
sc3 g (AHead a0 a1) c (THeads (Flat Appl) vs (lift (S i) O v))
→(getl i c (CHead d (Bind Abbr) v)
→sc3 g (AHead a0 a1) c (THeads (Flat Appl) vs (TLRef i)))
or equivalently
(land
arity g c (THeads (Flat Appl) vs (lift (S i) O v)) (AHead a0 a1)
∀d0:C
.∀w:T
.sc3 g a0 d0 w
→∀is:PList
.drop1 is d0 c
→(sc3
g
a1
d0
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (lift (S i) O v))))
→(getl i c (CHead d (Bind Abbr) v)
→sc3 g (AHead a0 a1) c (THeads (Flat Appl) vs (TLRef i)))
suppose H1:
land
arity g c (THeads (Flat Appl) vs (lift (S i) O v)) (AHead a0 a1)
∀d0:C
.∀w:T
.sc3 g a0 d0 w
→∀is:PList
.drop1 is d0 c
→(sc3
g
a1
d0
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (lift (S i) O v)))
suppose H2: getl i c (CHead d (Bind Abbr) v)
(H3) consider H1
we proceed by induction on H3 to prove
land
arity g c (THeads (Flat Appl) vs (TLRef i)) (AHead a0 a1)
∀d0:C
.∀w:T
.sc3 g a0 d0 w
→∀is:PList
.drop1 is d0 c
→(sc3
g
a1
d0
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (TLRef i)))
case conj : H4:arity g c (THeads (Flat Appl) vs (lift (S i) O v)) (AHead a0 a1) H5:∀d0:C.∀w:T.(sc3 g a0 d0 w)→∀is:PList.(drop1 is d0 c)→(sc3 g a1 d0 (THead (Flat Appl) w (lift1 is (THeads (Flat Appl) vs (lift (S i) O v))))) ⇒
the thesis becomes
land
arity g c (THeads (Flat Appl) vs (TLRef i)) (AHead a0 a1)
∀d0:C
.∀w:T
.sc3 g a0 d0 w
→∀is:PList
.drop1 is d0 c
→(sc3
g
a1
d0
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (TLRef i)))
(h1)
by (arity_appls_abbr . . . . . H2 . . H4)
arity g c (THeads (Flat Appl) vs (TLRef i)) (AHead a0 a1)
end of h1
(h2)
assume d0: C
assume w: T
suppose H6: sc3 g a0 d0 w
assume is: PList
suppose H7: drop1 is d0 c
(H_x)
by (drop1_getl_trans . . . H7 . . . . H2)
ex2
C
λe2:C.drop1 (ptrans is i) e2 d
λe2:C.getl (trans is i) d0 (CHead e2 (Bind Abbr) (lift1 (ptrans is i) v))
end of H_x
(H8) consider H_x
we proceed by induction on H8 to prove
sc3
g
a1
d0
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (TLRef i))
case ex_intro2 : x:C :drop1 (ptrans is i) x d H10:getl (trans is i) d0 (CHead x (Bind Abbr) (lift1 (ptrans is i) v)) ⇒
the thesis becomes
sc3
g
a1
d0
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (TLRef i))
(H_y)
by (H0 .)
∀i:nat
.∀d:C
.∀v:T
.∀c:C
.sc3 g a1 c (THeads (Flat Appl) (TCons w (lifts1 is vs)) (lift (S i) O v))
→(getl i c (CHead d (Bind Abbr) v)
→sc3 g a1 c (THeads (Flat Appl) (TCons w (lifts1 is vs)) (TLRef i)))
end of H_y
(h1)
(h1)
by (lift1_free . . .)
we proved
eq
T
lift1 is (lift (S i) O v)
lift (S (trans is i)) O (lift1 (ptrans is i) v)
we proceed by induction on the previous result to prove
sc3
g
a1
d0
THead
Flat Appl
w
THeads
Flat Appl
lifts1 is vs
lift (S (trans is i)) O (lift1 (ptrans is i) v)
case refl_equal : ⇒
the thesis becomes
sc3
g
a1
d0
THead
Flat Appl
w
THeads (Flat Appl) (lifts1 is vs) (lift1 is (lift (S i) O v))
by (lifts1_flat . . . .)
we proved
eq
T
lift1 is (THeads (Flat Appl) vs (lift (S i) O v))
THeads (Flat Appl) (lifts1 is vs) (lift1 is (lift (S i) O v))
we proceed by induction on the previous result to prove
sc3
g
a1
d0
THead
Flat Appl
w
THeads (Flat Appl) (lifts1 is vs) (lift1 is (lift (S i) O v))
case refl_equal : ⇒
the thesis becomes
sc3
g
a1
d0
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (lift (S i) O v))
by (H5 . . H6 . H7)
sc3
g
a1
d0
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (lift (S i) O v))
sc3
g
a1
d0
THead
Flat Appl
w
THeads (Flat Appl) (lifts1 is vs) (lift1 is (lift (S i) O v))
we proved
sc3
g
a1
d0
THead
Flat Appl
w
THeads
Flat Appl
lifts1 is vs
lift (S (trans is i)) O (lift1 (ptrans is i) v)
that is equivalent to
sc3
g
a1
d0
THeads
Flat Appl
TCons w (lifts1 is vs)
lift (S (trans is i)) O (lift1 (ptrans is i) v)
by (H_y . . . . previous H10)
we proved
sc3
g
a1
d0
THeads (Flat Appl) (TCons w (lifts1 is vs)) (TLRef (trans is i))
sc3
g
a1
d0
THead
Flat Appl
w
THeads (Flat Appl) (lifts1 is vs) (TLRef (trans is i))
end of h1
(h2)
by (lift1_lref . .)
eq T (lift1 is (TLRef i)) (TLRef (trans is i))
end of h2
by (eq_ind_r . . . h1 . h2)
sc3
g
a1
d0
THead
Flat Appl
w
THeads (Flat Appl) (lifts1 is vs) (lift1 is (TLRef i))
end of h1
(h2)
by (lifts1_flat . . . .)
eq
T
lift1 is (THeads (Flat Appl) vs (TLRef i))
THeads (Flat Appl) (lifts1 is vs) (lift1 is (TLRef i))
end of h2
by (eq_ind_r . . . h1 . h2)
sc3
g
a1
d0
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (TLRef i))
we proved
sc3
g
a1
d0
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (TLRef i))
∀d0:C
.∀w:T
.sc3 g a0 d0 w
→∀is:PList
.drop1 is d0 c
→(sc3
g
a1
d0
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (TLRef i)))
end of h2
by (conj . . h1 h2)
land
arity g c (THeads (Flat Appl) vs (TLRef i)) (AHead a0 a1)
∀d0:C
.∀w:T
.sc3 g a0 d0 w
→∀is:PList
.drop1 is d0 c
→(sc3
g
a1
d0
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (TLRef i)))
we proved
land
arity g c (THeads (Flat Appl) vs (TLRef i)) (AHead a0 a1)
∀d0:C
.∀w:T
.sc3 g a0 d0 w
→∀is:PList
.drop1 is d0 c
→(sc3
g
a1
d0
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (TLRef i)))
that is equivalent to sc3 g (AHead a0 a1) c (THeads (Flat Appl) vs (TLRef i))
we proved
(land
arity g c (THeads (Flat Appl) vs (lift (S i) O v)) (AHead a0 a1)
∀d0:C
.∀w:T
.sc3 g a0 d0 w
→∀is:PList
.drop1 is d0 c
→(sc3
g
a1
d0
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (lift (S i) O v))))
→(getl i c (CHead d (Bind Abbr) v)
→sc3 g (AHead a0 a1) c (THeads (Flat Appl) vs (TLRef i)))
that is equivalent to
sc3 g (AHead a0 a1) c (THeads (Flat Appl) vs (lift (S i) O v))
→(getl i c (CHead d (Bind Abbr) v)
→sc3 g (AHead a0 a1) c (THeads (Flat Appl) vs (TLRef i)))
∀vs:TList
.∀i:nat
.∀d:C
.∀v:T
.∀c:C
.sc3 g (AHead a0 a1) c (THeads (Flat Appl) vs (lift (S i) O v))
→(getl i c (CHead d (Bind Abbr) v)
→sc3 g (AHead a0 a1) c (THeads (Flat Appl) vs (TLRef i)))
we proved
∀vs:TList
.∀i:nat
.∀d:C
.∀v:T
.∀c:C
.sc3 g a c (THeads (Flat Appl) vs (lift (S i) O v))
→(getl i c (CHead d (Bind Abbr) v)
→sc3 g a c (THeads (Flat Appl) vs (TLRef i)))
we proved
∀g:G
.∀a:A
.∀vs:TList
.∀i:nat
.∀d:C
.∀v:T
.∀c:C
.sc3 g a c (THeads (Flat Appl) vs (lift (S i) O v))
→(getl i c (CHead d (Bind Abbr) v)
→sc3 g a c (THeads (Flat Appl) vs (TLRef i)))