---

Step * of Lemma csm-discrete-family

∀[A,B,s:Top].  ((discrete-family(A;a.B[a]))(s;q) ~ discrete-family(A;a.B[a]))
BY
{ (Intros THEN RepUR ``discrete-family csm-ap-type`` 0 THEN CsmUnfolding THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B,s:Top].    ((discrete-family(A;a.B[a]))(s;q)  \msim{}  discrete-family(A;a.B[a]))


By

---

Latex:
(Intros  THEN  RepUR  ``discrete-family  csm-ap-type``  0  THEN  CsmUnfolding  THEN  Auto)

---

Home Index