---

Step * of Lemma permutation-ss-eq

∀[rv,f,g,f',g':Top].  (<f, g> ≡ <f', g'> ~ ¬(fun-sep(rv;Point;f;f') ∨ fun-sep(rv;Point;g;g')))
BY
{ (Intros THEN Unfold `ss-eq` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[rv,f,g,f',g':Top].    (<f,  g>  \mequiv{}  <f',  g'>  \msim{}  \mneg{}(fun-sep(rv;Point;f;f')  \mvee{}  fun-sep(rv;Point;g;g')))


By

---

Latex:
(Intros  THEN  Unfold  `ss-eq`  0  THEN  Auto)

---

Home Index