---

Step * 1 of Lemma sq_stable__uiff


1. [P] : ℙ
2. [Q] : ℙ
3. SqStable(P)
4. SqStable(Q)
⊢ SqStable(uiff(P;Q))
BY
{ (Repeat (Unfolds ``iff rev_implies`` 0) THEN Auto) }

---

Latex:

---

Latex:

1.  [P]  :  \mBbbP{}
2.  [Q]  :  \mBbbP{}
3.  SqStable(P)
4.  SqStable(Q)
\mvdash{}  SqStable(uiff(P;Q))


By

---

Latex:
(Repeat  (Unfolds  ``iff  rev\_implies``  0)  THEN  Auto)

---

Home Index