---

Step * of Lemma iseg-global-order-loc

∀[Info:Type]. ∀L1,L2:(Id × Info) List.  (L1 ≤ L2 ⇒ (∀e:E. (loc(e) = loc(e) ∈ Id)))
BY
{ (Intros THEN (FLemma `iseg_length` [-2] THENA 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||
⊢ loc(e) = loc(e) ∈ Id

---

Latex:

---

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


By

---

Latex:
(Intros  THEN  (FLemma  `iseg\_length`  [-2]  THENA  Auto))

---

Home Index