---

Step * of Lemma csm+-comp-csm+-sq

No Annotations
∀[H,K,X,A,tau,s:Top].  (tau+ o s+ ~ tau o s+)
BY
{ (Auto THEN CsmUnfolding THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[H,K,X,A,tau,s:Top].    (tau+  o  s+  \msim{}  tau  o  s+)


By

---

Latex:
(Auto  THEN  CsmUnfolding  THEN  Auto)

---

Home Index