---

Step * of Lemma comb_for_set_blt_wf

λp,a,b,z. (a <b b) ∈ p:PosetSig ⟶ a:|p| ⟶ b:|p| ⟶ (↓True) ⟶ 𝔹
BY
{ ProveOpCombTyping `set_blt_wf` }

---

Latex:

---

Latex:
\mlambda{}p,a,b,z.  (a  <\msubb{}  b)  \mmember{}  p:PosetSig  {}\mrightarrow{}  a:|p|  {}\mrightarrow{}  b:|p|  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  \mBbbB{}


By

---

Latex:
ProveOpCombTyping  `set\_blt\_wf`

---

Home Index