---

Step * of Lemma iseg-es-embedding

∀[Info:Type]. ∀L1,L2:(Id × Info) List.  (L1 ≤ L2 ⇒ (λx.x embeds global-eo(L1) into global-eo(L2)))
BY
{ (Auto THEN (FLemma `iseg_length` [-1] THENA Auto) THEN D 0 THEN Auto THEN Reduce 0) }

1
1. Info : Type
2. L1 : (Id × Info) List@i
3. L2 : (Id × Info) List@i
4. L1 ≤ L2@i
5. ||L1|| ≤ ||L2||
⊢ es-local-embedding(Info;global-eo(L1);global-eo(L2);λx.x)

2
1. Info : Type
2. L1 : (Id × Info) List@i
3. L2 : (Id × Info) List@i
4. L1 ≤ L2@i
5. ||L1|| ≤ ||L2||
6. e : E@i
7. e' : E@i
8. (e' < e)@i
⊢ (e' < e)

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}L1,L2:(Id  \mtimes{}  Info)  List.    (L1  \mleq{}  L2  {}\mRightarrow{}  (\mlambda{}x.x  embeds  global-eo(L1)  into  global-eo(L2)))


By

---

Latex:
(Auto  THEN  (FLemma  `iseg\_length`  [-1]  THENA  Auto)  THEN  D  0  THEN  Auto  THEN  Reduce  0)

---

Home Index