DEFINITION lifts1_xhg()
TYPE =
∀hds:PList
.∀ts:TList
.eq
TList
lifts1 (Ss hds) (lifts (S O) O ts)
lifts (S O) O (lifts1 hds ts)
BODY =
assume hds: PList
assume ts: TList
we proceed by induction on ts to prove
eq
TList
lifts1 (Ss hds) (lifts (S O) O ts)
lifts (S O) O (lifts1 hds ts)
case TNil : ⇒
the thesis becomes
eq
TList
lifts1 (Ss hds) (lifts (S O) O TNil)
lifts (S O) O (lifts1 hds TNil)
by (refl_equal . .)
we proved eq TList TNil TNil
eq
TList
lifts1 (Ss hds) (lifts (S O) O TNil)
lifts (S O) O (lifts1 hds TNil)
case TCons : t:T t0:TList ⇒
the thesis becomes
eq
TList
lifts1 (Ss hds) (lifts (S O) O (TCons t t0))
lifts (S O) O (lifts1 hds (TCons t t0))
(H) by induction hypothesis we know
eq TList (lifts1 (Ss hds) (lifts (S O) O t0)) (lifts (S O) O (lifts1 hds t0))
(h1)
by (refl_equal . .)
we proved
eq
TList
TCons (lift (S O) O (lift1 hds t)) (lifts (S O) O (lifts1 hds t0))
TCons (lift (S O) O (lift1 hds t)) (lifts (S O) O (lifts1 hds t0))
by (eq_ind_r . . . previous . H)
eq
TList
TCons (lift (S O) O (lift1 hds t)) (lifts1 (Ss hds) (lifts (S O) O t0))
TCons (lift (S O) O (lift1 hds t)) (lifts (S O) O (lifts1 hds t0))
end of h1
(h2)
by (lift1_xhg . .)
eq T (lift1 (Ss hds) (lift (S O) O t)) (lift (S O) O (lift1 hds t))
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
eq
TList
TCons
lift1 (Ss hds) (lift (S O) O t)
lifts1 (Ss hds) (lifts (S O) O t0)
TCons (lift (S O) O (lift1 hds t)) (lifts (S O) O (lifts1 hds t0))
eq
TList
lifts1 (Ss hds) (lifts (S O) O (TCons t t0))
lifts (S O) O (lifts1 hds (TCons t t0))
we proved
eq
TList
lifts1 (Ss hds) (lifts (S O) O ts)
lifts (S O) O (lifts1 hds ts)
we proved
∀hds:PList
.∀ts:TList
.eq
TList
lifts1 (Ss hds) (lifts (S O) O ts)
lifts (S O) O (lifts1 hds ts)