---

Step * 1 1 2 1 2 of Lemma Girard-theorem


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)
BY
{ TACTIC:(With ⌜max-WO{i:l}()⌝ (D 0)⋅ THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
TACTIC:(With  \mkleeneopen{}max-WO\{i:l\}()\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index