---

Step * 2 of Lemma es-rank_le


1. es : EO
2. e1 : E
3. e2 : E
4. e1 = e2 ∈ E
⊢ es-rank(es;e1) ≤ es-rank(es;e2)
BY
{ (HypSubst' (-1) 0 THEN Auto) }

---

Latex:



1.  es  :  EO
2.  e1  :  E
3.  e2  :  E
4.  e1  =  e2
\mvdash{}  es-rank(es;e1)  \mleq{}  es-rank(es;e2)


By

(HypSubst'  (-1)  0  THEN  Auto)

---

Home Index