---

Step * of Lemma iseg-global-order-history

∀[Info:Type]
  ∀L1,L2:(Id × Info) List.  (L1 ≤ L2 ⇒ (∀e:E. (map(λx.info(x);≤loc(e)) = map(λx.info(x);≤loc(e)) ∈ Info List+)))
BY
{ ((Intros THEN (FLemma `iseg_length` [-2] THENA Auto))
   THEN (Assert loc(e) = loc(e) ∈ Id BY
               (BLemma `iseg-global-order-loc` THEN Auto))
   ) }

1
1. Info : Type
2. L1 : (Id × Info) List@i
3. L2 : (Id × Info) List@i
4. L1 ≤ L2@i
5. e : E@i
6. ||L1|| ≤ ||L2||
7. loc(e) = loc(e) ∈ Id
⊢ map(λx.info(x);≤loc(e)) = map(λx.info(x);≤loc(e)) ∈ Info List+

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}L1,L2:(Id  \mtimes{}  Info)  List.    (L1  \mleq{}  L2  {}\mRightarrow{}  (\mforall{}e:E.  (map(\mlambda{}x.info(x);\mleq{}loc(e))  =  map(\mlambda{}x.info(x);\mleq{}loc(e)))))


By

---

Latex:
((Intros  THEN  (FLemma  `iseg\_length`  [-2]  THENA  Auto))
  THEN  (Assert  loc(e)  =  loc(e)  BY
                          (BLemma  `iseg-global-order-loc`  THEN  Auto))
  )

---

Home Index