---

Step * of Lemma prod-ss-sep

∀[ss1,ss2,x,y:Top].  (x # y ~ fst(x) # fst(y) ∨ snd(x) # snd(y))
BY
{ (Auto THEN Computation) }

---

Latex:

---

Latex:
\mforall{}[ss1,ss2,x,y:Top].    (x  \#  y  \msim{}  fst(x)  \#  fst(y)  \mvee{}  snd(x)  \#  snd(y))


By

---

Latex:
(Auto  THEN  Computation)

---

Home Index