DEFINITION sc3_arity_csubc()
TYPE =
∀g:G
.∀c1:C
.∀t:T
.∀a:A
.arity g c1 t a
→∀d1:C.∀is:PList.(drop1 is d1 c1)→∀c2:C.(csubc g d1 c2)→(sc3 g a c2 (lift1 is t))
BODY =
assume g: G
assume c1: C
assume t: T
assume a: A
suppose H: arity g c1 t a
we proceed by induction on H to prove ∀d1:C.∀is:PList.(drop1 is d1 c1)→∀c2:C.(csubc g d1 c2)→(sc3 g a c2 (lift1 is t))
case arity_sort : c:C n:nat ⇒
the thesis becomes
∀d1:C
.∀is:PList
.drop1 is d1 c
→∀c2:C
.csubc g d1 c2
→(land
arity g c2 (lift1 is (TSort n)) (ASort O n)
sn3 c2 (lift1 is (TSort n)))
assume d1: C
assume is: PList
suppose : drop1 is d1 c
assume c2: C
suppose : csubc g d1 c2
(h1)
(h1)
by (arity_sort . . .)
arity g c2 (TSort n) (ASort O n)
end of h1
(h2)
by (nf2_sort . .)
we proved nf2 c2 (TSort n)
by (sn3_nf2 . . previous)
sn3 c2 (TSort n)
end of h2
by (conj . . h1 h2)
land (arity g c2 (TSort n) (ASort O n)) (sn3 c2 (TSort n))
end of h1
(h2)
by (lift1_sort . .)
eq T (lift1 is (TSort n)) (TSort n)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
land
arity g c2 (lift1 is (TSort n)) (ASort O n)
sn3 c2 (lift1 is (TSort n))
that is equivalent to sc3 g (ASort O n) c2 (lift1 is (TSort n))
∀d1:C
.∀is:PList
.drop1 is d1 c
→∀c2:C
.csubc g d1 c2
→(land
arity g c2 (lift1 is (TSort n)) (ASort O n)
sn3 c2 (lift1 is (TSort n)))
case arity_abbr : c:C d:C u:T i:nat H0:getl i c (CHead d (Bind Abbr) u) a0:A :arity g d u a0 ⇒
the thesis becomes ∀d1:C.∀is:PList.∀H3:(drop1 is d1 c).∀c2:C.∀H4:(csubc g d1 c2).(sc3 g a0 c2 (lift1 is (TLRef i)))
(H2) by induction hypothesis we know ∀d1:C.∀is:PList.(drop1 is d1 d)→∀c2:C.(csubc g d1 c2)→(sc3 g a0 c2 (lift1 is u))
assume d1: C
assume is: PList
suppose H3: drop1 is d1 c
assume c2: C
suppose H4: csubc g d1 c2
(H_x)
by (drop1_getl_trans . . . H3 . . . . H0)
ex2
C
λe2:C.drop1 (ptrans is i) e2 d
λe2:C.getl (trans is i) d1 (CHead e2 (Bind Abbr) (lift1 (ptrans is i) u))
end of H_x
(H5) consider H_x
we proceed by induction on H5 to prove sc3 g a0 c2 (lift1 is (TLRef i))
case ex_intro2 : x:C :drop1 (ptrans is i) x d H7:getl (trans is i) d1 (CHead x (Bind Abbr) (lift1 (ptrans is i) u)) ⇒
the thesis becomes sc3 g a0 c2 (lift1 is (TLRef i))
(H_x0)
by (csubc_getl_conf . . . . H7 . H4)
ex2
C
λe2:C.getl (trans is i) c2 e2
λe2:C.csubc g (CHead x (Bind Abbr) (lift1 (ptrans is i) u)) e2
end of H_x0
(H8) consider H_x0
we proceed by induction on H8 to prove sc3 g a0 c2 (lift1 is (TLRef i))
case ex_intro2 : x0:C H9:getl (trans is i) c2 x0 H10:csubc g (CHead x (Bind Abbr) (lift1 (ptrans is i) u)) x0 ⇒
the thesis becomes sc3 g a0 c2 (lift1 is (TLRef i))
(H_x1)
by (csubc_gen_head_l . . . . . H10)
or3
ex2
C
λc2:C.eq C x0 (CHead c2 (Bind Abbr) (lift1 (ptrans is i) u))
λc2:C.csubc g x c2
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K (Bind Abbr) (Bind Abst)
λc2:C.λw:T.λ:A.eq C x0 (CHead c2 (Bind Abbr) w)
λc2:C.λ:T.λ:A.csubc g x c2
λ:C.λ:T.λa:A.sc3 g (asucc g a) x (lift1 (ptrans is i) u)
λc2:C.λw:T.λa:A.sc3 g a c2 w
ex4_3
B
C
T
λb:B.λc2:C.λv2:T.eq C x0 (CHead c2 (Bind b) v2)
λ:B.λ:C.λ:T.eq K (Bind Abbr) (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc2:C.λ:T.csubc g x c2
end of H_x1
(H11) consider H_x1
we proceed by induction on H11 to prove sc3 g a0 c2 (lift1 is (TLRef i))
case or3_intro0 : H12:ex2 C λc3:C.eq C x0 (CHead c3 (Bind Abbr) (lift1 (ptrans is i) u)) λc3:C.csubc g x c3 ⇒
the thesis becomes sc3 g a0 c2 (lift1 is (TLRef i))
we proceed by induction on H12 to prove sc3 g a0 c2 (lift1 is (TLRef i))
case ex_intro2 : x1:C H13:eq C x0 (CHead x1 (Bind Abbr) (lift1 (ptrans is i) u)) :csubc g x x1 ⇒
the thesis becomes sc3 g a0 c2 (lift1 is (TLRef i))
(H15)
we proceed by induction on H13 to prove getl (trans is i) c2 (CHead x1 (Bind Abbr) (lift1 (ptrans is i) u))
case refl_equal : ⇒
the thesis becomes the hypothesis H9
getl (trans is i) c2 (CHead x1 (Bind Abbr) (lift1 (ptrans is i) u))
end of H15
(H_y)
by (sc3_abbr . . .)
∀i:nat
.∀d:C
.∀v:T
.∀c:C
.sc3 g a0 c (THeads (Flat Appl) TNil (lift (S i) O v))
→(getl i c (CHead d (Bind Abbr) v)
→sc3 g a0 c (THeads (Flat Appl) TNil (TLRef i)))
end of H_y
(h1)
by (lift1_free . . .)
we proved
eq
T
lift1 is (lift (S i) O u)
lift (S (trans is i)) O (lift1 (ptrans is i) u)
we proceed by induction on the previous result to prove sc3 g a0 c2 (lift (S (trans is i)) O (lift1 (ptrans is i) u))
case refl_equal : ⇒
the thesis becomes sc3 g a0 c2 (lift1 is (lift (S i) O u))
by (lift1_cons_tail . . . .)
we proved eq T (lift1 (PConsTail is (S i) O) u) (lift1 is (lift (S i) O u))
we proceed by induction on the previous result to prove sc3 g a0 c2 (lift1 is (lift (S i) O u))
case refl_equal : ⇒
the thesis becomes sc3 g a0 c2 (lift1 (PConsTail is (S i) O) u)
by (getl_drop . . . . . H0)
we proved drop (S i) O c d
by (drop1_cons_tail . . . . previous . . H3)
we proved drop1 (PConsTail is (S i) O) d1 d
by (H2 . . previous . H4)
sc3 g a0 c2 (lift1 (PConsTail is (S i) O) u)
sc3 g a0 c2 (lift1 is (lift (S i) O u))
we proved sc3 g a0 c2 (lift (S (trans is i)) O (lift1 (ptrans is i) u))
that is equivalent to
sc3
g
a0
c2
THeads
Flat Appl
TNil
lift (S (trans is i)) O (lift1 (ptrans is i) u)
by (H_y . . . . previous H15)
we proved sc3 g a0 c2 (THeads (Flat Appl) TNil (TLRef (trans is i)))
sc3 g a0 c2 (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 a0 c2 (lift1 is (TLRef i))
sc3 g a0 c2 (lift1 is (TLRef i))
case or3_intro1 : H12:ex5_3 C T A λ:C.λ:T.λ:A.eq K (Bind Abbr) (Bind Abst) λc3:C.λw:T.λ:A.eq C x0 (CHead c3 (Bind Abbr) w) λc3:C.λ:T.λ:A.csubc g x c3 λ:C.λ:T.λa1:A.sc3 g (asucc g a1) x (lift1 (ptrans is i) u) λc3:C.λw:T.λa1:A.sc3 g a1 c3 w ⇒
the thesis becomes sc3 g a0 c2 (lift1 is (TLRef i))
we proceed by induction on H12 to prove sc3 g a0 c2 (lift1 is (TLRef i))
case ex5_3_intro : x1:C x2:T x3:A H13:eq K (Bind Abbr) (Bind Abst) H14:eq C x0 (CHead x1 (Bind Abbr) x2) :csubc g x x1 :sc3 g (asucc g x3) x (lift1 (ptrans is i) u) :sc3 g x3 x1 x2 ⇒
the thesis becomes sc3 g a0 c2 (lift1 is (TLRef i))
(H19)
we proceed by induction on H13 to prove
<λ:K.Prop>
CASE Bind Abst OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒True | Abst⇒False | Void⇒False
| Flat ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:K.Prop>
CASE Bind Abbr OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒True | Abst⇒False | Void⇒False
| Flat ⇒False
consider I
we proved True
<λ:K.Prop>
CASE Bind Abbr OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒True | Abst⇒False | Void⇒False
| Flat ⇒False
<λ:K.Prop>
CASE Bind Abst OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒True | Abst⇒False | Void⇒False
| Flat ⇒False
end of H19
consider H19
we proved
<λ:K.Prop>
CASE Bind Abst OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒True | Abst⇒False | Void⇒False
| Flat ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove sc3 g a0 c2 (lift1 is (TLRef i))
sc3 g a0 c2 (lift1 is (TLRef i))
sc3 g a0 c2 (lift1 is (TLRef i))
case or3_intro2 : H12:ex4_3 B C T λb:B.λc3:C.λv2:T.eq C x0 (CHead c3 (Bind b) v2) λ:B.λ:C.λ:T.eq K (Bind Abbr) (Bind Void) λb:B.λ:C.λ:T.not (eq B b Void) λ:B.λc3:C.λ:T.csubc g x c3 ⇒
the thesis becomes sc3 g a0 c2 (lift1 is (TLRef i))
we proceed by induction on H12 to prove sc3 g a0 c2 (lift1 is (TLRef i))
case ex4_3_intro : x1:B x2:C x3:T H13:eq C x0 (CHead x2 (Bind x1) x3) H14:eq K (Bind Abbr) (Bind Void) :not (eq B x1 Void) :csubc g x x2 ⇒
the thesis becomes sc3 g a0 c2 (lift1 is (TLRef i))
(H18)
we proceed by induction on H14 to prove
<λ:K.Prop>
CASE Bind Void OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒True | Abst⇒False | Void⇒False
| Flat ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:K.Prop>
CASE Bind Abbr OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒True | Abst⇒False | Void⇒False
| Flat ⇒False
consider I
we proved True
<λ:K.Prop>
CASE Bind Abbr OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒True | Abst⇒False | Void⇒False
| Flat ⇒False
<λ:K.Prop>
CASE Bind Void OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒True | Abst⇒False | Void⇒False
| Flat ⇒False
end of H18
consider H18
we proved
<λ:K.Prop>
CASE Bind Void OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒True | Abst⇒False | Void⇒False
| Flat ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove sc3 g a0 c2 (lift1 is (TLRef i))
sc3 g a0 c2 (lift1 is (TLRef i))
sc3 g a0 c2 (lift1 is (TLRef i))
sc3 g a0 c2 (lift1 is (TLRef i))
sc3 g a0 c2 (lift1 is (TLRef i))
we proved sc3 g a0 c2 (lift1 is (TLRef i))
∀d1:C.∀is:PList.∀H3:(drop1 is d1 c).∀c2:C.∀H4:(csubc g d1 c2).(sc3 g a0 c2 (lift1 is (TLRef i)))
case arity_abst : c:C d:C u:T i:nat H0:getl i c (CHead d (Bind Abst) u) a0:A H1:arity g d u (asucc g a0) ⇒
the thesis becomes ∀d1:C.∀is:PList.∀H3:(drop1 is d1 c).∀c2:C.∀H4:(csubc g d1 c2).(sc3 g a0 c2 (lift1 is (TLRef i)))
() by induction hypothesis we know ∀d1:C.∀is:PList.(drop1 is d1 d)→∀c2:C.(csubc g d1 c2)→(sc3 g (asucc g a0) c2 (lift1 is u))
assume d1: C
assume is: PList
suppose H3: drop1 is d1 c
assume c2: C
suppose H4: csubc g d1 c2
(H5) consider H0
(H_x)
by (drop1_getl_trans . . . H3 . . . . H5)
ex2
C
λe2:C.drop1 (ptrans is i) e2 d
λe2:C.getl (trans is i) d1 (CHead e2 (Bind Abst) (lift1 (ptrans is i) u))
end of H_x
(H6) consider H_x
we proceed by induction on H6 to prove sc3 g a0 c2 (lift1 is (TLRef i))
case ex_intro2 : x:C H7:drop1 (ptrans is i) x d H8:getl (trans is i) d1 (CHead x (Bind Abst) (lift1 (ptrans is i) u)) ⇒
the thesis becomes sc3 g a0 c2 (lift1 is (TLRef i))
(H_x0)
by (csubc_getl_conf . . . . H8 . H4)
ex2
C
λe2:C.getl (trans is i) c2 e2
λe2:C.csubc g (CHead x (Bind Abst) (lift1 (ptrans is i) u)) e2
end of H_x0
(H9) consider H_x0
we proceed by induction on H9 to prove sc3 g a0 c2 (lift1 is (TLRef i))
case ex_intro2 : x0:C H10:getl (trans is i) c2 x0 H11:csubc g (CHead x (Bind Abst) (lift1 (ptrans is i) u)) x0 ⇒
the thesis becomes sc3 g a0 c2 (lift1 is (TLRef i))
(H_x1)
by (csubc_gen_head_l . . . . . H11)
or3
ex2
C
λc2:C.eq C x0 (CHead c2 (Bind Abst) (lift1 (ptrans is i) u))
λc2:C.csubc g x c2
ex5_3
C
T
A
λ:C.λ:T.λ:A.eq K (Bind Abst) (Bind Abst)
λc2:C.λw:T.λ:A.eq C x0 (CHead c2 (Bind Abbr) w)
λc2:C.λ:T.λ:A.csubc g x c2
λ:C.λ:T.λa:A.sc3 g (asucc g a) x (lift1 (ptrans is i) u)
λc2:C.λw:T.λa:A.sc3 g a c2 w
ex4_3
B
C
T
λb:B.λc2:C.λv2:T.eq C x0 (CHead c2 (Bind b) v2)
λ:B.λ:C.λ:T.eq K (Bind Abst) (Bind Void)
λb:B.λ:C.λ:T.not (eq B b Void)
λ:B.λc2:C.λ:T.csubc g x c2
end of H_x1
(H12) consider H_x1
we proceed by induction on H12 to prove sc3 g a0 c2 (lift1 is (TLRef i))
case or3_intro0 : H13:ex2 C λc3:C.eq C x0 (CHead c3 (Bind Abst) (lift1 (ptrans is i) u)) λc3:C.csubc g x c3 ⇒
the thesis becomes sc3 g a0 c2 (lift1 is (TLRef i))
we proceed by induction on H13 to prove sc3 g a0 c2 (lift1 is (TLRef i))
case ex_intro2 : x1:C H14:eq C x0 (CHead x1 (Bind Abst) (lift1 (ptrans is i) u)) :csubc g x x1 ⇒
the thesis becomes sc3 g a0 c2 (lift1 is (TLRef i))
(H16)
we proceed by induction on H14 to prove getl (trans is i) c2 (CHead x1 (Bind Abst) (lift1 (ptrans is i) u))
case refl_equal : ⇒
the thesis becomes the hypothesis H10
getl (trans is i) c2 (CHead x1 (Bind Abst) (lift1 (ptrans is i) u))
end of H16
(H_y)
by (sc3_abst . . .)
∀c:C
.∀i:nat
.arity g c (THeads (Flat Appl) TNil (TLRef i)) a0
→(nf2 c (TLRef i)
→(sns3 c TNil)→(sc3 g a0 c (THeads (Flat Appl) TNil (TLRef i))))
end of H_y
(h1)
(h1)
by (lift1_lref . .)
we proved eq T (lift1 is (TLRef i)) (TLRef (trans is i))
we proceed by induction on the previous result to prove arity g d1 (TLRef (trans is i)) a0
case refl_equal : ⇒
the thesis becomes arity g d1 (lift1 is (TLRef i)) a0
by (arity_abst . . . . . H0 . H1)
we proved arity g c (TLRef i) a0
by (arity_lift1 . . . . . . H3 previous)
arity g d1 (lift1 is (TLRef i)) a0
we proved arity g d1 (TLRef (trans is i)) a0
by (csubc_arity_conf . . . H4 . . previous)
we proved arity g c2 (TLRef (trans is i)) a0
arity g c2 (THeads (Flat Appl) TNil (TLRef (trans is i))) a0
end of h1
(h2)
by (nf2_lref_abst . . . . H16)
nf2 c2 (TLRef (trans is i))
end of h2
(h3)
consider I
we proved True
sns3 c2 TNil
end of h3
by (H_y . . h1 h2 h3)
we proved sc3 g a0 c2 (THeads (Flat Appl) TNil (TLRef (trans is i)))
sc3 g a0 c2 (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 a0 c2 (lift1 is (TLRef i))
sc3 g a0 c2 (lift1 is (TLRef i))
case or3_intro1 : H13:ex5_3 C T A λ:C.λ:T.λ:A.eq K (Bind Abst) (Bind Abst) λc3:C.λw:T.λ:A.eq C x0 (CHead c3 (Bind Abbr) w) λc3:C.λ:T.λ:A.csubc g x c3 λ:C.λ:T.λa1:A.sc3 g (asucc g a1) x (lift1 (ptrans is i) u) λc3:C.λw:T.λa1:A.sc3 g a1 c3 w ⇒
the thesis becomes sc3 g a0 c2 (lift1 is (TLRef i))
we proceed by induction on H13 to prove sc3 g a0 c2 (lift1 is (TLRef i))
case ex5_3_intro : x1:C x2:T x3:A :eq K (Bind Abst) (Bind Abst) H15:eq C x0 (CHead x1 (Bind Abbr) x2) :csubc g x x1 H17:sc3 g (asucc g x3) x (lift1 (ptrans is i) u) H18:sc3 g x3 x1 x2 ⇒
the thesis becomes sc3 g a0 c2 (lift1 is (TLRef i))
(H19)
we proceed by induction on H15 to prove getl (trans is i) c2 (CHead x1 (Bind Abbr) x2)
case refl_equal : ⇒
the thesis becomes the hypothesis H10
getl (trans is i) c2 (CHead x1 (Bind Abbr) x2)
end of H19
(H_y)
by (sc3_abbr . . .)
∀i:nat
.∀d:C
.∀v:T
.∀c:C
.sc3 g a0 c (THeads (Flat Appl) TNil (lift (S i) O v))
→(getl i c (CHead d (Bind Abbr) v)
→sc3 g a0 c (THeads (Flat Appl) TNil (TLRef i)))
end of H_y
(h1)
(H_y0)
by (arity_lift1 . . . . . . H7 H1)
arity g x (lift1 (ptrans is i) u) (asucc g a0)
end of H_y0
(H_y1)
by (sc3_arity_gen . . . . H17)
arity g x (lift1 (ptrans is i) u) (asucc g x3)
end of H_y1
(h1)
by (getl_drop . . . . . H19)
we proved drop (S (trans is i)) O c2 x1
by (sc3_lift . . . . H18 . . . previous)
sc3 g x3 c2 (lift (S (trans is i)) O x2)
end of h1
(h2)
by (arity_mono . . . . H_y1 . H_y0)
we proved leq g (asucc g x3) (asucc g a0)
by (asucc_inj . . . previous)
leq g x3 a0
end of h2
by (sc3_repl . . . . h1 . h2)
we proved sc3 g a0 c2 (lift (S (trans is i)) O x2)
that is equivalent to sc3 g a0 c2 (THeads (Flat Appl) TNil (lift (S (trans is i)) O x2))
by (H_y . . . . previous H19)
we proved sc3 g a0 c2 (THeads (Flat Appl) TNil (TLRef (trans is i)))
sc3 g a0 c2 (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 a0 c2 (lift1 is (TLRef i))
sc3 g a0 c2 (lift1 is (TLRef i))
case or3_intro2 : H13:ex4_3 B C T λb:B.λc3:C.λv2:T.eq C x0 (CHead c3 (Bind b) v2) λ:B.λ:C.λ:T.eq K (Bind Abst) (Bind Void) λb:B.λ:C.λ:T.not (eq B b Void) λ:B.λc3:C.λ:T.csubc g x c3 ⇒
the thesis becomes sc3 g a0 c2 (lift1 is (TLRef i))
we proceed by induction on H13 to prove sc3 g a0 c2 (lift1 is (TLRef i))
case ex4_3_intro : x1:B x2:C x3:T H14:eq C x0 (CHead x2 (Bind x1) x3) H15:eq K (Bind Abst) (Bind Void) :not (eq B x1 Void) :csubc g x x2 ⇒
the thesis becomes sc3 g a0 c2 (lift1 is (TLRef i))
(H19)
we proceed by induction on H15 to prove
<λ:K.Prop>
CASE Bind Void OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:K.Prop>
CASE Bind Abst OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
consider I
we proved True
<λ:K.Prop>
CASE Bind Abst OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
<λ:K.Prop>
CASE Bind Void OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
end of H19
consider H19
we proved
<λ:K.Prop>
CASE Bind Void OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove sc3 g a0 c2 (lift1 is (TLRef i))
sc3 g a0 c2 (lift1 is (TLRef i))
sc3 g a0 c2 (lift1 is (TLRef i))
sc3 g a0 c2 (lift1 is (TLRef i))
sc3 g a0 c2 (lift1 is (TLRef i))
we proved sc3 g a0 c2 (lift1 is (TLRef i))
∀d1:C.∀is:PList.∀H3:(drop1 is d1 c).∀c2:C.∀H4:(csubc g d1 c2).(sc3 g a0 c2 (lift1 is (TLRef i)))
case arity_bind : b:B H0:not (eq B b Abst) c:C u:T a1:A :arity g c u a1 t0:T a2:A :arity g (CHead c (Bind b) u) t0 a2 ⇒
the thesis becomes ∀d1:C.∀is:PList.∀H5:(drop1 is d1 c).∀c2:C.∀H6:(csubc g d1 c2).(sc3 g a2 c2 (lift1 is (THead (Bind b) u t0)))
(H2) by induction hypothesis we know ∀d1:C.∀is:PList.(drop1 is d1 c)→∀c2:C.(csubc g d1 c2)→(sc3 g a1 c2 (lift1 is u))
(H4) by induction hypothesis we know
∀d1:C
.∀is:PList
.(drop1 is d1 (CHead c (Bind b) u))→∀c2:C.(csubc g d1 c2)→(sc3 g a2 c2 (lift1 is t0))
assume d1: C
assume is: PList
suppose H5: drop1 is d1 c
assume c2: C
suppose H6: csubc g d1 c2
(H_y)
by (sc3_bind . . H0 . . .)
∀c:C
.∀v:T
.∀t:T
.(sc3
g
a2
CHead c (Bind b) v
THeads (Flat Appl) (lifts (S O) O TNil) t)
→(sc3 g a1 c v
→sc3 g a2 c (THeads (Flat Appl) TNil (THead (Bind b) v t)))
end of H_y
(h1)
(h1)
(h1)
by (drop1_skip_bind . . . . . H5)
drop1 (Ss is) (CHead d1 (Bind b) (lift1 is u)) (CHead c (Bind b) u)
end of h1
(h2)
by (csubc_head . . . H6 . .)
csubc g (CHead d1 (Bind b) (lift1 is u)) (CHead c2 (Bind b) (lift1 is u))
end of h2
by (H4 . . h1 . h2)
we proved sc3 g a2 (CHead c2 (Bind b) (lift1 is u)) (lift1 (Ss is) t0)
sc3
g
a2
CHead c2 (Bind b) (lift1 is u)
THeads (Flat Appl) (lifts (S O) O TNil) (lift1 (Ss is) t0)
end of h1
(h2) by (H2 . . H5 . H6) we proved sc3 g a1 c2 (lift1 is u)
by (H_y . . . h1 h2)
we proved
sc3
g
a2
c2
THeads
Flat Appl
TNil
THead (Bind b) (lift1 is u) (lift1 (Ss is) t0)
sc3 g a2 c2 (THead (Bind b) (lift1 is u) (lift1 (Ss is) t0))
end of h1
(h2)
by (lift1_bind . . . .)
eq
T
lift1 is (THead (Bind b) u t0)
THead (Bind b) (lift1 is u) (lift1 (Ss is) t0)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved sc3 g a2 c2 (lift1 is (THead (Bind b) u t0))
∀d1:C.∀is:PList.∀H5:(drop1 is d1 c).∀c2:C.∀H6:(csubc g d1 c2).(sc3 g a2 c2 (lift1 is (THead (Bind b) u t0)))
case arity_head : c:C u:T a1:A H0:arity g c u (asucc g a1) t0:T a2:A H2:arity g (CHead c (Bind Abst) u) t0 a2 ⇒
the thesis becomes
∀d1:C
.∀is:PList
.∀H4:drop1 is d1 c
.∀c2:C
.∀H5:csubc g d1 c2
.land
arity g c2 (lift1 is (THead (Bind Abst) u t0)) (AHead a1 a2)
∀d:C
.∀w:T
.sc3 g a1 d w
→∀is0:PList
.drop1 is0 d c2
→sc3 g a2 d (THead (Flat Appl) w (lift1 is0 (lift1 is (THead (Bind Abst) u t0))))
(H1) by induction hypothesis we know ∀d1:C.∀is:PList.(drop1 is d1 c)→∀c2:C.(csubc g d1 c2)→(sc3 g (asucc g a1) c2 (lift1 is u))
(H3) by induction hypothesis we know
∀d1:C
.∀is:PList
.(drop1 is d1 (CHead c (Bind Abst) u))→∀c2:C.(csubc g d1 c2)→(sc3 g a2 c2 (lift1 is t0))
assume d1: C
assume is: PList
suppose H4: drop1 is d1 c
assume c2: C
suppose H5: csubc g d1 c2
(h1)
(h1)
(h1)
by (arity_lift1 . . . . . . H4 H0)
arity g d1 (lift1 is u) (asucc g a1)
end of h1
(h2)
by (drop1_skip_bind . . . . . H4)
we proved
drop1
Ss is
CHead d1 (Bind Abst) (lift1 is u)
CHead c (Bind Abst) u
by (arity_lift1 . . . . . . previous H2)
arity g (CHead d1 (Bind Abst) (lift1 is u)) (lift1 (Ss is) t0) a2
end of h2
by (arity_head . . . . h1 . . h2)
we proved arity g d1 (THead (Bind Abst) (lift1 is u) (lift1 (Ss is) t0)) (AHead a1 a2)
by (csubc_arity_conf . . . H5 . . previous)
arity g c2 (THead (Bind Abst) (lift1 is u) (lift1 (Ss is) t0)) (AHead a1 a2)
end of h1
(h2)
assume d: C
assume w: T
suppose H6: sc3 g a1 d w
assume is0: PList
suppose H7: drop1 is0 d c2
(h1)
(H8)
by (sc3_appl . . . .)
∀c:C
.∀v:T
.∀t:T
.sc3 g a2 c (THeads (Flat Appl) TNil (THead (Bind Abbr) v t))
→(sc3 g a1 c v
→∀w:T
.sc3 g (asucc g a1) c w
→(sc3
g
a2
c
THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind Abst) w t)))
end of H8
(h1)
(H_y)
we must prove not (eq B Abbr Abst)
or equivalently (eq B Abbr Abst)→False
suppose H9: eq B Abbr Abst
by (not_abbr_abst H9)
we proved False
we proved (eq B Abbr Abst)→False
that is equivalent to not (eq B Abbr Abst)
by (sc3_bind . . previous . . .)
∀c:C
.∀v:T
.∀t:T
.(sc3
g
a2
CHead c (Bind Abbr) v
THeads (Flat Appl) (lifts (S O) O TNil) t)
→(sc3 g a1 c v
→sc3 g a2 c (THeads (Flat Appl) TNil (THead (Bind Abbr) v t)))
end of H_y
(H_x)
by (csubc_drop1_conf_rev . . . . H7 . H5)
ex2 C λc1:C.drop1 is0 c1 d1 λc1:C.csubc g c1 d
end of H_x
(H9) consider H_x
we proceed by induction on H9 to prove sc3 g a2 (CHead d (Bind Abbr) w) (lift1 (Ss is0) (lift1 (Ss is) t0))
case ex_intro2 : x:C H10:drop1 is0 x d1 H11:csubc g x d ⇒
the thesis becomes sc3 g a2 (CHead d (Bind Abbr) w) (lift1 (Ss is0) (lift1 (Ss is) t0))
(h1)
(h1)
(h1)
by (drop1_trans . . . H10 . . H4)
we proved drop1 (papp is0 is) x c
by (drop1_skip_bind . . . . . previous)
drop1
Ss (papp is0 is)
CHead x (Bind Abst) (lift1 (papp is0 is) u)
CHead c (Bind Abst) u
end of h1
(h2)
(h1)
by (drop1_trans . . . H10 . . H4)
drop1 (papp is0 is) x c
end of h1
(h2)
by (csubc_refl . .)
csubc g x x
end of h2
by (H1 . . h1 . h2)
we proved sc3 g (asucc g a1) x (lift1 (papp is0 is) u)
by (csubc_abst . . . H11 . . previous . H6)
csubc
g
CHead x (Bind Abst) (lift1 (papp is0 is) u)
CHead d (Bind Abbr) w
end of h2
by (H3 . . h1 . h2)
sc3 g a2 (CHead d (Bind Abbr) w) (lift1 (Ss (papp is0 is)) t0)
end of h1
(h2)
by (papp_ss . .)
eq PList (papp (Ss is0) (Ss is)) (Ss (papp is0 is))
end of h2
by (eq_ind_r . . . h1 . h2)
sc3 g a2 (CHead d (Bind Abbr) w) (lift1 (papp (Ss is0) (Ss is)) t0)
end of h1
(h2)
by (lift1_lift1 . . .)
eq T (lift1 (Ss is0) (lift1 (Ss is) t0)) (lift1 (papp (Ss is0) (Ss is)) t0)
end of h2
by (eq_ind_r . . . h1 . h2)
sc3 g a2 (CHead d (Bind Abbr) w) (lift1 (Ss is0) (lift1 (Ss is) t0))
we proved sc3 g a2 (CHead d (Bind Abbr) w) (lift1 (Ss is0) (lift1 (Ss is) t0))
that is equivalent to
sc3
g
a2
CHead d (Bind Abbr) w
THeads
Flat Appl
lifts (S O) O TNil
lift1 (Ss is0) (lift1 (Ss is) t0)
by (H_y . . . previous H6)
sc3
g
a2
d
THeads
Flat Appl
TNil
THead (Bind Abbr) w (lift1 (Ss is0) (lift1 (Ss is) t0))
end of h1
(h2)
by (H1 . . H4 . H5)
we proved sc3 g (asucc g a1) c2 (lift1 is u)
by (sc3_lift1 . . . . . . previous H7)
sc3 g (asucc g a1) d (lift1 is0 (lift1 is u))
end of h2
by (H8 . . . h1 H6 . h2)
we proved
sc3
g
a2
d
THeads
Flat Appl
TNil
THead
Flat Appl
w
THead (Bind Abst) (lift1 is0 (lift1 is u)) (lift1 (Ss is0) (lift1 (Ss is) t0))
sc3
g
a2
d
THead
Flat Appl
w
THead (Bind Abst) (lift1 is0 (lift1 is u)) (lift1 (Ss is0) (lift1 (Ss is) t0))
end of h1
(h2)
by (lift1_bind . . . .)
eq
T
lift1 is0 (THead (Bind Abst) (lift1 is u) (lift1 (Ss is) t0))
THead (Bind Abst) (lift1 is0 (lift1 is u)) (lift1 (Ss is0) (lift1 (Ss is) t0))
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
sc3
g
a2
d
THead
Flat Appl
w
lift1 is0 (THead (Bind Abst) (lift1 is u) (lift1 (Ss is) t0))
∀d:C
.∀w:T
.sc3 g a1 d w
→∀is0:PList
.drop1 is0 d c2
→(sc3
g
a2
d
THead
Flat Appl
w
lift1 is0 (THead (Bind Abst) (lift1 is u) (lift1 (Ss is) t0)))
end of h2
by (conj . . h1 h2)
land
arity g c2 (THead (Bind Abst) (lift1 is u) (lift1 (Ss is) t0)) (AHead a1 a2)
∀d:C
.∀w:T
.sc3 g a1 d w
→∀is0:PList
.drop1 is0 d c2
→(sc3
g
a2
d
THead
Flat Appl
w
lift1 is0 (THead (Bind Abst) (lift1 is u) (lift1 (Ss is) t0)))
end of h1
(h2)
by (lift1_bind . . . .)
eq
T
lift1 is (THead (Bind Abst) u t0)
THead (Bind Abst) (lift1 is u) (lift1 (Ss is) t0)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
land
arity g c2 (lift1 is (THead (Bind Abst) u t0)) (AHead a1 a2)
∀d:C
.∀w:T
.sc3 g a1 d w
→∀is0:PList
.drop1 is0 d c2
→sc3 g a2 d (THead (Flat Appl) w (lift1 is0 (lift1 is (THead (Bind Abst) u t0))))
that is equivalent to sc3 g (AHead a1 a2) c2 (lift1 is (THead (Bind Abst) u t0))
∀d1:C
.∀is:PList
.∀H4:drop1 is d1 c
.∀c2:C
.∀H5:csubc g d1 c2
.land
arity g c2 (lift1 is (THead (Bind Abst) u t0)) (AHead a1 a2)
∀d:C
.∀w:T
.sc3 g a1 d w
→∀is0:PList
.drop1 is0 d c2
→sc3 g a2 d (THead (Flat Appl) w (lift1 is0 (lift1 is (THead (Bind Abst) u t0))))
case arity_appl : c:C u:T a1:A :arity g c u a1 t0:T a2:A :arity g c t0 (AHead a1 a2) ⇒
the thesis becomes ∀d1:C.∀is:PList.∀H4:(drop1 is d1 c).∀c2:C.∀H5:(csubc g d1 c2).(sc3 g a2 c2 (lift1 is (THead (Flat Appl) u t0)))
(H1) by induction hypothesis we know ∀d1:C.∀is:PList.(drop1 is d1 c)→∀c2:C.(csubc g d1 c2)→(sc3 g a1 c2 (lift1 is u))
(H3) by induction hypothesis we know ∀d1:C.∀is:PList.(drop1 is d1 c)→∀c2:C.(csubc g d1 c2)→(sc3 g (AHead a1 a2) c2 (lift1 is t0))
assume d1: C
assume is: PList
suppose H4: drop1 is d1 c
assume c2: C
suppose H5: csubc g d1 c2
(H_y) by (H1 . . H4 . H5) we proved sc3 g a1 c2 (lift1 is u)
(H_y0)
by (H3 . . H4 . H5)
sc3 g (AHead a1 a2) c2 (lift1 is t0)
end of H_y0
(H6) consider H_y0
consider H6
we proved sc3 g (AHead a1 a2) c2 (lift1 is t0)
that is equivalent to
land
arity g c2 (lift1 is t0) (AHead a1 a2)
∀d:C
.∀w:T
.sc3 g a1 d w
→∀is0:PList.(drop1 is0 d c2)→(sc3 g a2 d (THead (Flat Appl) w (lift1 is0 (lift1 is t0))))
we proceed by induction on the previous result to prove sc3 g a2 c2 (lift1 is (THead (Flat Appl) u t0))
case conj : :arity g c2 (lift1 is t0) (AHead a1 a2) H8:∀d:C.∀w:T.(sc3 g a1 d w)→∀is0:PList.(drop1 is0 d c2)→(sc3 g a2 d (THead (Flat Appl) w (lift1 is0 (lift1 is t0)))) ⇒
the thesis becomes sc3 g a2 c2 (lift1 is (THead (Flat Appl) u t0))
(H_y1)
by (H8 . . H_y .)
(drop1 PNil c2 c2)→(sc3 g a2 c2 (THead (Flat Appl) (lift1 is u) (lift1 PNil (lift1 is t0))))
end of H_y1
(h1)
by (drop1_nil .)
we proved drop1 PNil c2 c2
by (H_y1 previous)
we proved sc3 g a2 c2 (THead (Flat Appl) (lift1 is u) (lift1 PNil (lift1 is t0)))
sc3 g a2 c2 (THead (Flat Appl) (lift1 is u) (lift1 is t0))
end of h1
(h2)
by (lift1_flat . . . .)
eq
T
lift1 is (THead (Flat Appl) u t0)
THead (Flat Appl) (lift1 is u) (lift1 is t0)
end of h2
by (eq_ind_r . . . h1 . h2)
sc3 g a2 c2 (lift1 is (THead (Flat Appl) u t0))
we proved sc3 g a2 c2 (lift1 is (THead (Flat Appl) u t0))
∀d1:C.∀is:PList.∀H4:(drop1 is d1 c).∀c2:C.∀H5:(csubc g d1 c2).(sc3 g a2 c2 (lift1 is (THead (Flat Appl) u t0)))
case arity_cast : c:C u:T a0:A :arity g c u (asucc g a0) t0:T :arity g c t0 a0 ⇒
the thesis becomes ∀d1:C.∀is:PList.∀H4:(drop1 is d1 c).∀c2:C.∀H5:(csubc g d1 c2).(sc3 g a0 c2 (lift1 is (THead (Flat Cast) u t0)))
(H1) by induction hypothesis we know ∀d1:C.∀is:PList.(drop1 is d1 c)→∀c2:C.(csubc g d1 c2)→(sc3 g (asucc g a0) c2 (lift1 is u))
(H3) by induction hypothesis we know ∀d1:C.∀is:PList.(drop1 is d1 c)→∀c2:C.(csubc g d1 c2)→(sc3 g a0 c2 (lift1 is t0))
assume d1: C
assume is: PList
suppose H4: drop1 is d1 c
assume c2: C
suppose H5: csubc g d1 c2
(H_y)
by (sc3_cast . . .)
∀c:C
.∀u:T
.sc3 g (asucc g a0) c (THeads (Flat Appl) TNil u)
→∀t:T
.sc3 g a0 c (THeads (Flat Appl) TNil t)
→sc3 g a0 c (THeads (Flat Appl) TNil (THead (Flat Cast) u t))
end of H_y
(h1)
(h1)
by (H1 . . H4 . H5)
we proved sc3 g (asucc g a0) c2 (lift1 is u)
sc3 g (asucc g a0) c2 (THeads (Flat Appl) TNil (lift1 is u))
end of h1
(h2)
by (H3 . . H4 . H5)
we proved sc3 g a0 c2 (lift1 is t0)
sc3 g a0 c2 (THeads (Flat Appl) TNil (lift1 is t0))
end of h2
by (H_y . . h1 . h2)
we proved
sc3
g
a0
c2
THeads (Flat Appl) TNil (THead (Flat Cast) (lift1 is u) (lift1 is t0))
sc3 g a0 c2 (THead (Flat Cast) (lift1 is u) (lift1 is t0))
end of h1
(h2)
by (lift1_flat . . . .)
eq
T
lift1 is (THead (Flat Cast) u t0)
THead (Flat Cast) (lift1 is u) (lift1 is t0)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved sc3 g a0 c2 (lift1 is (THead (Flat Cast) u t0))
∀d1:C.∀is:PList.∀H4:(drop1 is d1 c).∀c2:C.∀H5:(csubc g d1 c2).(sc3 g a0 c2 (lift1 is (THead (Flat Cast) u t0)))
case arity_repl : c:C t0:T a1:A :arity g c t0 a1 a2:A H2:leq g a1 a2 ⇒
the thesis becomes ∀d1:C.∀is:PList.∀H3:(drop1 is d1 c).∀c2:C.∀H4:(csubc g d1 c2).(sc3 g a2 c2 (lift1 is t0))
(H1) by induction hypothesis we know ∀d1:C.∀is:PList.(drop1 is d1 c)→∀c2:C.(csubc g d1 c2)→(sc3 g a1 c2 (lift1 is t0))
assume d1: C
assume is: PList
suppose H3: drop1 is d1 c
assume c2: C
suppose H4: csubc g d1 c2
by (H1 . . H3 . H4)
we proved sc3 g a1 c2 (lift1 is t0)
by (sc3_repl . . . . previous . H2)
we proved sc3 g a2 c2 (lift1 is t0)
∀d1:C.∀is:PList.∀H3:(drop1 is d1 c).∀c2:C.∀H4:(csubc g d1 c2).(sc3 g a2 c2 (lift1 is t0))
we proved ∀d1:C.∀is:PList.(drop1 is d1 c1)→∀c2:C.(csubc g d1 c2)→(sc3 g a c2 (lift1 is t))
we proved
∀g:G
.∀c1:C
.∀t:T
.∀a:A
.arity g c1 t a
→∀d1:C.∀is:PList.(drop1 is d1 c1)→∀c2:C.(csubc g d1 c2)→(sc3 g a c2 (lift1 is t))