---

Step * of Lemma es-causle_weakening_eq

∀es:EO. ∀a,b:E.  a c≤ b supposing a = b ∈ E
BY
{ Auto }

1
1. es : EO@i'
2. a : E@i
3. b : E@i
4. a = b ∈ E
⊢ a c≤ b

---

Latex:


\mforall{}es:EO.  \mforall{}a,b:E.    a  c\mleq{}  b  supposing  a  =  b


By

Auto

---

Home Index