Step
*
of Lemma
pscm-adjoin-id-adjoin
∀[B,xx,s,X,Y,Z:Top]. (((B)(s o p;q))[xx] ~ (B)(s;xx))
BY
{ (Intros THEN RW (SubC (SymbCompC [] 100)) 0 THEN Auto) }
Latex:
Latex:
\mforall{}[B,xx,s,X,Y,Z:Top]. (((B)(s o p;q))[xx] \msim{} (B)(s;xx))
By
Latex:
(Intros THEN RW (SubC (SymbCompC [] 100)) 0 THEN Auto)
Home
Index