---

Step * 1 1 2 of Lemma Girard-theorem


1. Type ∈ Type
2. WFO{i:l}() ∈ Type
3. max-WO{i:l}() ∈ WFO{i:l}()
⊢ False
BY
{ TACTIC:Assert ⌜∃v:WFO{i:l}(). (v order-type-less() v)⌝⋅ }

1
.....assertion..... 
1. Type ∈ Type
2. WFO{i:l}() ∈ Type
3. max-WO{i:l}() ∈ WFO{i:l}()
⊢ ∃v:WFO{i:l}(). (v order-type-less() v)

2
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

---

Latex:

---

Latex:

1.  Type  \mmember{}  Type
2.  WFO\{i:l\}()  \mmember{}  Type
3.  max-WO\{i:l\}()  \mmember{}  WFO\{i:l\}()
\mvdash{}  False


By

---

Latex:
TACTIC:Assert  \mkleeneopen{}\mexists{}v:WFO\{i:l\}().  (v  order-type-less()  v)\mkleeneclose{}\mcdot{}

---

Home Index