---

Step * of Lemma squash_functionality_wrt_iff

∀[P,Q:ℙ].  ({P ⇐⇒ Q} ⇒ {↓P ⇐⇒ ↓Q})
BY
{ ((((Unfold `guard` 0 THENM RepeatMFor 4 (D 0)) THENM BLemma `squash_functionality_wrt_implies`) THENM HypBackchain)
   THENA Auto
   ) }

---

Latex:

---

Latex:
\mforall{}[P,Q:\mBbbP{}].    (\{P  \mLeftarrow{}{}\mRightarrow{}  Q\}  {}\mRightarrow{}  \{\mdownarrow{}P  \mLeftarrow{}{}\mRightarrow{}  \mdownarrow{}Q\})


By

---

Latex:
((((Unfold  `guard`  0  THENM  RepeatMFor  4  (D  0))  THENM  BLemma  `squash\_functionality\_wrt\_implies`)
  THENM  HypBackchain
  )
  THENA  Auto
  )

---

Home Index