---

Step * 1 1 2 2 of Lemma Girard-theorem


1. Type ∈ Type
2. WFO{i:l}() ∈ Type
3. max-WO{i:l}() ∈ WFO{i:l}()
4. ∃v:WFO{i:l}(). (v order-type-less() v)
⊢ False
BY
{ TACTIC:(D -1 THEN InstLemma `DCC-order-type-less-ext` [] THEN (With ⌜λn.v⌝ (D (-1))⋅ THENA Auto) THEN Reduce (-1)) }

1
1. Type ∈ Type
2. WFO{i:l}() ∈ Type
3. max-WO{i:l}() ∈ WFO{i:l}()
4. v : WFO{i:l}()
5. v order-type-less() v
6. ¬(∀i:ℕ. (v order-type-less() v))
⊢ False

---

Latex:

---

Latex:

1.  Type  \mmember{}  Type
2.  WFO\{i:l\}()  \mmember{}  Type
3.  max-WO\{i:l\}()  \mmember{}  WFO\{i:l\}()
4.  \mexists{}v:WFO\{i:l\}().  (v  order-type-less()  v)
\mvdash{}  False


By

---

Latex:
TACTIC:(D  -1
                THEN  InstLemma  `DCC-order-type-less-ext`  []
                THEN  (With  \mkleeneopen{}\mlambda{}n.v\mkleeneclose{}  (D  (-1))\mcdot{}  THENA  Auto)
                THEN  Reduce  (-1))

---

Home Index