---

Step * of Lemma set_le_wf

∀[p:PosetSig]. (≤b ∈ |p| ⟶ |p| ⟶ 𝔹)
BY
{ ModulePiTac 3 ``set_car set_eq set_le`` }

---

Latex:

---

Latex:
\mforall{}[p:PosetSig].  (\mleq{}\msubb{}  \mmember{}  |p|  {}\mrightarrow{}  |p|  {}\mrightarrow{}  \mBbbB{})


By

---

Latex:
ModulePiTac  3  ``set\_car  set\_eq  set\_le``

---

Home Index