---

Step * of Lemma order-type-less_wf

order-type-less() ∈ WFO{i:l}() ⟶ WFO{i:l}() ⟶ ℙ'
BY
{ (Unfold `WFO` 0 THEN ProveWfLemma) }

---

Latex:

---

Latex:
order-type-less()  \mmember{}  WFO\{i:l\}()  {}\mrightarrow{}  WFO\{i:l\}()  {}\mrightarrow{}  \mBbbP{}'


By

---

Latex:
(Unfold  `WFO`  0  THEN  ProveWfLemma)

---

Home Index