---

Step * of Lemma csm-case-endpoints

∀[a,b,r,s:Top].  (([r=0 ⊢→ a; r=1 ⊢→ b])s ~ [(r)s=0 ⊢→ (a)s; (r)s=1 ⊢→ (b)s])
BY
{ (Intros THEN RepUR ``case-endpoints`` 0 THEN RWW "csm-case-term csm-face-zero" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a,b,r,s:Top].    (([r=0  \mvdash{}\mrightarrow{}  a;  r=1  \mvdash{}\mrightarrow{}  b])s  \msim{}  [(r)s=0  \mvdash{}\mrightarrow{}  (a)s;  (r)s=1  \mvdash{}\mrightarrow{}  (b)s])


By

---

Latex:
(Intros  THEN  RepUR  ``case-endpoints``  0  THEN  RWW  "csm-case-term  csm-face-zero"  0  THEN  Auto)

---

Home Index