---

Step * of Lemma squash_functionality_wrt_implies

∀[P,Q:ℙ].  ({P ⇒ Q} ⇒ {(↓P) ⇒ (↓Q)})
BY
{ ((Unfold `guard` 0 THEN RepD) THENA Auto) }

1
1. P : ℙ
2. Q : ℙ
3. P ⇒ Q@i
4. ↓P@i
⊢ ↓Q

---

Latex:

---

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


By

---

Latex:
((Unfold  `guard`  0  THEN  RepD)  THENA  Auto)

---

Home Index