---

Step * of Lemma DCC-order-type-less

DCC(WFO{i:l}();order-type-less())
BY
{ (Unfold `WFO` 0 THEN RepeatFor 2 ((D 0 THENW Auto))) }

1
1. f : ℕ ⟶ (A:Type × <:A ⟶ A ⟶ ℙ × DCC(A;<))
2. ∀i:ℕ. ((f (i + 1)) order-type-less() (f i))
⊢ False

---

Latex:

---

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


By

---

Latex:
(Unfold  `WFO`  0  THEN  RepeatFor  2  ((D  0  THENW  Auto)))

---

Home Index