---

Step * 1 1 2 1 of Lemma Girard-theorem

.....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)
BY
{ TACTIC:(RenameVar `trans' 3⋅ THEN InstLemma `order-type-less-maximal-ext` [⌜max-WFTO{i:l}()⌝]⋅ THEN Reduce (-1)) }

1
.....wf..... 
1. Type ∈ Type
2. WFO{i:l}() ∈ Type
3. trans : max-WO{i:l}() ∈ WFO{i:l}()
⊢ max-WFTO{i:l}() ∈ WFTRO{i:l}()

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

---

Latex:

---

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


By

---

Latex:
TACTIC:(RenameVar  `trans'  3\mcdot{}
                THEN  InstLemma  `order-type-less-maximal-ext`  [\mkleeneopen{}max-WFTO\{i:l\}()\mkleeneclose{}]\mcdot{}
                THEN  Reduce  (-1))

---

Home Index