---

Step * of Lemma set_car_wf

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

---

Latex:

---

Latex:
\mforall{}[p:PosetSig].  (|p|  \mmember{}  Type)


By

---

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

---

Home Index