---

Step * 1 of Lemma DCC-order-type_wf


1. TERMOF{DCC-order-type-less-ext:o, \\v:l, i:l} ∈ DCC(WFO{i:l}();order-type-less())
⊢ DCC-order-type() ∈ DCC(WFO{i:l}();order-type-less())
BY
{ (RW (AddrC [2] (TagC (mk_tag_term 1))) (-1) THEN Trivial) }

---

Latex:

---

Latex:

1.  TERMOF\{DCC-order-type-less-ext:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}  \mmember{}  DCC(WFO\{i:l\}();order-type-less())
\mvdash{}  DCC-order-type()  \mmember{}  DCC(WFO\{i:l\}();order-type-less())


By

---

Latex:
(RW  (AddrC  [2]  (TagC  (mk\_tag\_term  1)))  (-1)  THEN  Trivial)

---

Home Index