Step * of Lemma es-locl-irreflex-test

[es:EO]. ∀[e2,e:E].  ¬(e e2 ∈ E) supposing (e <loc e2)
BY
Auto }


Latex:


\mforall{}[es:EO].  \mforall{}[e2,e:E].    \mneg{}(e  =  e2)  supposing  (e  <loc  e2)


By

Auto




Home Index