---

Step * of Lemma DCC-order-type-less-ext

DCC(WFO{i:l}();order-type-less())
BY
{ Extract of Obid: DCC-order-type-less
  not unfolding  primrec
  finishing with xxxTry ((Fold `DCC-order-type` 0 THEN Auto))xxx
  normalizes to:
  
  DCC-order-type() }

---

Latex:

---

Latex:
DCC(WFO\{i:l\}();order-type-less())


By

---

Latex:
Extract  of  Obid:  DCC-order-type-less
not  unfolding    primrec
finishing  with  xxxTry  ((Fold  `DCC-order-type`  0  THEN  Auto))xxx
normalizes  to:

DCC-order-type()

---

Home Index