---

Step * of Lemma comb_for_bimplies_wf

λp,q,z. (p ⇒b q) ∈ p:𝔹 ⟶ q:𝔹 supposing ↑p ⟶ (↓True) ⟶ 𝔹
BY
{ (ProveOpCombinatorTyping Auto) `bimplies_wf` }

---

Latex:

---

Latex:
\mlambda{}p,q,z.  (p  {}\mRightarrow{}\msubb{}  q)  \mmember{}  p:\mBbbB{}  {}\mrightarrow{}  q:\mBbbB{}  supposing  \muparrow{}p  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  \mBbbB{}


By

---

Latex:
(ProveOpCombinatorTyping  Auto)  `bimplies\_wf`

---

Home Index