---

Step * of Lemma comb_for_iff_wf

λA,B,z. (A ⇐⇒ B) ∈ A:ℙ ⟶ B:ℙ ⟶ (↓True) ⟶ ℙ
BY
{ (ProveOpCombinatorTyping Auto{1,3}-1) `iff_wf` }

---

Latex:

---

Latex:
\mlambda{}A,B,z.  (A  \mLeftarrow{}{}\mRightarrow{}  B)  \mmember{}  A:\mBbbP{}  {}\mrightarrow{}  B:\mBbbP{}  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  \mBbbP{}


By

---

Latex:
(ProveOpCombinatorTyping  Auto\{1,3\}-1)  `iff\_wf`

---

Home Index