DEFINITION sc3_lift()
TYPE =
∀g:G
.∀a:A
.∀e:C
.∀t:T
.(sc3 g a e t)→∀c:C.∀h:nat.∀d:nat.(drop h d c e)→(sc3 g a c (lift h d t))
BODY =
assume g: G
assume a: A
we proceed by induction on a to prove
∀e:C
.∀t:T
.(sc3 g a e t)→∀c:C.∀h:nat.∀d:nat.(drop h d c e)→(sc3 g a c (lift h d t))
case ASort : n:nat n0:nat ⇒
the thesis becomes
∀e:C
.∀t:T
.sc3 g (ASort n n0) e t
→∀c:C.∀h:nat.∀d:nat.(drop h d c e)→(sc3 g (ASort n n0) c (lift h d t))
assume e: C
assume t: T
we must prove
sc3 g (ASort n n0) e t
→∀c:C.∀h:nat.∀d:nat.(drop h d c e)→(sc3 g (ASort n n0) c (lift h d t))
or equivalently
land (arity g e t (ASort n n0)) (sn3 e t)
→∀c:C.∀h:nat.∀d:nat.(drop h d c e)→(sc3 g (ASort n n0) c (lift h d t))
suppose H: land (arity g e t (ASort n n0)) (sn3 e t)
assume c: C
assume h: nat
assume d: nat
suppose H0: drop h d c e
(H1) consider H
we proceed by induction on H1 to prove land (arity g c (lift h d t) (ASort n n0)) (sn3 c (lift h d t))
case conj : H2:arity g e t (ASort n n0) H3:sn3 e t ⇒
the thesis becomes land (arity g c (lift h d t) (ASort n n0)) (sn3 c (lift h d t))
(h1)
by (arity_lift . . . . H2 . . . H0)
arity g c (lift h d t) (ASort n n0)
end of h1
(h2)
by (sn3_lift . . H3 . . . H0)
sn3 c (lift h d t)
end of h2
by (conj . . h1 h2)
land (arity g c (lift h d t) (ASort n n0)) (sn3 c (lift h d t))
we proved land (arity g c (lift h d t) (ASort n n0)) (sn3 c (lift h d t))
that is equivalent to sc3 g (ASort n n0) c (lift h d t)
we proved
land (arity g e t (ASort n n0)) (sn3 e t)
→∀c:C.∀h:nat.∀d:nat.(drop h d c e)→(sc3 g (ASort n n0) c (lift h d t))
that is equivalent to
sc3 g (ASort n n0) e t
→∀c:C.∀h:nat.∀d:nat.(drop h d c e)→(sc3 g (ASort n n0) c (lift h d t))
∀e:C
.∀t:T
.sc3 g (ASort n n0) e t
→∀c:C.∀h:nat.∀d:nat.(drop h d c e)→(sc3 g (ASort n n0) c (lift h d t))
case AHead : a0:A a1:A ⇒
the thesis becomes
∀e:C
.∀t:T
.sc3 g (AHead a0 a1) e t
→∀c:C.∀h:nat.∀d:nat.(drop h d c e)→(sc3 g (AHead a0 a1) c (lift h d t))
() by induction hypothesis we know
∀e:C
.∀t:T.(sc3 g a0 e t)→∀c:C.∀h:nat.∀d:nat.(drop h d c e)→(sc3 g a0 c (lift h d t))
() by induction hypothesis we know
∀e:C
.∀t:T.(sc3 g a1 e t)→∀c:C.∀h:nat.∀d:nat.(drop h d c e)→(sc3 g a1 c (lift h d t))
assume e: C
assume t: T
we must prove
sc3 g (AHead a0 a1) e t
→∀c:C.∀h:nat.∀d:nat.(drop h d c e)→(sc3 g (AHead a0 a1) c (lift h d t))
or equivalently
(land
arity g e t (AHead a0 a1)
∀d:C
.∀w:T
.sc3 g a0 d w
→∀is:PList.(drop1 is d e)→(sc3 g a1 d (THead (Flat Appl) w (lift1 is t))))
→∀c:C.∀h:nat.∀d:nat.(drop h d c e)→(sc3 g (AHead a0 a1) c (lift h d t))
suppose H1:
land
arity g e t (AHead a0 a1)
∀d:C
.∀w:T
.sc3 g a0 d w
→∀is:PList.(drop1 is d e)→(sc3 g a1 d (THead (Flat Appl) w (lift1 is t)))
assume c: C
assume h: nat
assume d: nat
suppose H2: drop h d c e
(H3) consider H1
we proceed by induction on H3 to prove
land
arity g c (lift h d t) (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 (lift h d t))))
case conj : H4:arity g e t (AHead a0 a1) H5:∀d0:C.∀w:T.(sc3 g a0 d0 w)→∀is:PList.(drop1 is d0 e)→(sc3 g a1 d0 (THead (Flat Appl) w (lift1 is t))) ⇒
the thesis becomes
land
arity g c (lift h d t) (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 (lift h d t))))
(h1)
by (arity_lift . . . . H4 . . . H2)
arity g c (lift h d t) (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_y)
by (H5 . . H6 .)
drop1 (PConsTail is h d) d0 e
→sc3 g a1 d0 (THead (Flat Appl) w (lift1 (PConsTail is h d) t))
end of H_y
by (lift1_cons_tail . . . .)
we proved eq T (lift1 (PConsTail is h d) t) (lift1 is (lift h d t))
we proceed by induction on the previous result to prove sc3 g a1 d0 (THead (Flat Appl) w (lift1 is (lift h d t)))
case refl_equal : ⇒
the thesis becomes sc3 g a1 d0 (THead (Flat Appl) w (lift1 (PConsTail is h d) t))
by (drop1_cons_tail . . . . H2 . . H7)
we proved drop1 (PConsTail is h d) d0 e
by (H_y previous)
sc3 g a1 d0 (THead (Flat Appl) w (lift1 (PConsTail is h d) t))
we proved sc3 g a1 d0 (THead (Flat Appl) w (lift1 is (lift h d t)))
∀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 (lift h d t))))
end of h2
by (conj . . h1 h2)
land
arity g c (lift h d t) (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 (lift h d t))))
we proved
land
arity g c (lift h d t) (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 (lift h d t))))
that is equivalent to sc3 g (AHead a0 a1) c (lift h d t)
we proved
(land
arity g e t (AHead a0 a1)
∀d:C
.∀w:T
.sc3 g a0 d w
→∀is:PList.(drop1 is d e)→(sc3 g a1 d (THead (Flat Appl) w (lift1 is t))))
→∀c:C.∀h:nat.∀d:nat.(drop h d c e)→(sc3 g (AHead a0 a1) c (lift h d t))
that is equivalent to
sc3 g (AHead a0 a1) e t
→∀c:C.∀h:nat.∀d:nat.(drop h d c e)→(sc3 g (AHead a0 a1) c (lift h d t))
∀e:C
.∀t:T
.sc3 g (AHead a0 a1) e t
→∀c:C.∀h:nat.∀d:nat.(drop h d c e)→(sc3 g (AHead a0 a1) c (lift h d t))
we proved
∀e:C
.∀t:T
.(sc3 g a e t)→∀c:C.∀h:nat.∀d:nat.(drop h d c e)→(sc3 g a c (lift h d t))
we proved
∀g:G
.∀a:A
.∀e:C
.∀t:T
.(sc3 g a e t)→∀c:C.∀h:nat.∀d:nat.(drop h d c e)→(sc3 g a c (lift h d t))