---

Step * of Lemma comb_for_band_wf

λp,q,z. (p ∧b q) ∈ p:𝔹 ⟶ q:𝔹 ⟶ (↓True) ⟶ 𝔹
BY
{ (ProveOpCombinatorTyping Auto{1,3}-1) `band_wf` }

---

Latex:

---

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


By

---

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

---

Home Index