Step
*
of Lemma
sq_stable__implies
∀[P,Q:ℙ].  (SqStable(Q) 
⇒ SqStable(P 
⇒ Q))
BY
{ (Unfold `sq_stable` 0 THEN skip{Auto}) }
1
∀[P,Q:ℙ].  (((↓Q) 
⇒ Q) 
⇒ (↓P 
⇒ Q) 
⇒ P 
⇒ Q)
Latex:
Latex:
\mforall{}[P,Q:\mBbbP{}].    (SqStable(Q)  {}\mRightarrow{}  SqStable(P  {}\mRightarrow{}  Q))
By
Latex:
(Unfold  `sq\_stable`  0  THEN  skip\{Auto\})
Home
Index