---

Step * of Lemma fun-ss-sep

∀[ss,A,f,g:Top].  (f # g ~ ∃a:A. f a # g a)
BY
{ (Auto THEN Computation) }

---

Latex:

---

Latex:
\mforall{}[ss,A,f,g:Top].    (f  \#  g  \msim{}  \mexists{}a:A.  f  a  \#  g  a)


By

---

Latex:
(Auto  THEN  Computation)

---

Home Index