---

Step * of Lemma comb_for_bor_wf

λp,q,z. (p ∨bq) ∈ p:𝔹 ⟶ q:𝔹 ⟶ (↓True) ⟶ 𝔹
BY
{ (ProveOpCombinatorTyping Auto{1,3}-1) `bor_wf` }

---

Latex:

---

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


By

---

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

---

Home Index