---

Step * of Lemma psc-fst-pscm-adjoin-sq

∀[Gamma,Delta,X,sigma,u:Top].  (p o (sigma;u) ~ sigma o 1(Delta))
BY
{ (Intros THEN UseWitness ⌜Ax⌝⋅ THEN MemCD THEN PscmUnfolding THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Gamma,Delta,X,sigma,u:Top].    (p  o  (sigma;u)  \msim{}  sigma  o  1(Delta))


By

---

Latex:
(Intros  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}  THEN  MemCD  THEN  PscmUnfolding  THEN  Auto)

---

Home Index