---

Step * 1 of Lemma p-pscm+-type


1. H : Top
2. K : Top
3. A : Top
4. B : Top
5. tau : Top
⊢ ((A)p)tau+ ~ ((A)tau)p
BY
{ (RW (SubC (SymbCompC [] 100)) 0 THEN Auto) }

---

Latex:

---

Latex:

1.  H  :  Top
2.  K  :  Top
3.  A  :  Top
4.  B  :  Top
5.  tau  :  Top
\mvdash{}  ((A)p)tau+  \msim{}  ((A)tau)p


By

---

Latex:
(RW  (SubC  (SymbCompC  []  100))  0  THEN  Auto)

---

Home Index