---

Step * of Lemma csm-case-term

∀[phi,u,v,s:Top].  (((u ∨ v))s ~ ((u)s ∨ (v)s))
BY
{ (Intros THEN RepUR ``case-term`` 0 THEN CsmUnfolding THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[phi,u,v,s:Top].    (((u  \mvee{}  v))s  \msim{}  ((u)s  \mvee{}  (v)s))


By

---

Latex:
(Intros  THEN  RepUR  ``case-term``  0  THEN  CsmUnfolding  THEN  Auto)

---

Home Index