---

Step * 1 1 of Lemma global-eo-eq-E


1. L : (Id × Top) List
2. a : ℕ||L||
3. b : ℕ||L||
⊢ fst(L[a]) = fst(L[b]) ∧b (¬ba <z b) ∧b (¬bb <z a) = (a =z b)
BY
{ Auto }

---

Latex:

---

Latex:

1.  L  :  (Id  \mtimes{}  Top)  List
2.  a  :  \mBbbN{}||L||
3.  b  :  \mBbbN{}||L||
\mvdash{}  fst(L[a])  =  fst(L[b])  \mwedge{}\msubb{}  (\mneg{}\msubb{}a  <z  b)  \mwedge{}\msubb{}  (\mneg{}\msubb{}b  <z  a)  =  (a  =\msubz{}  b)


By

---

Latex:
Auto

---

Home Index