---

Step * 1 1 2 2 1 1 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}()
5. p : v order-type-less() v
6. f : ¬(∀i:ℕ. (v order-type-less() v))
⊢ False
BY
{ TACTIC:UseWitness ⌜f (λn.p)⌝⋅ }

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

---

Latex:

---

Latex:

1.  Type  \mmember{}  Type
2.  WFO\{i:l\}()  \mmember{}  Type
3.  max-WO\{i:l\}()  \mmember{}  WFO\{i:l\}()
4.  v  :  WFO\{i:l\}()
5.  p  :  v  order-type-less()  v
6.  f  :  \mneg{}(\mforall{}i:\mBbbN{}.  (v  order-type-less()  v))
\mvdash{}  False


By

---

Latex:
TACTIC:UseWitness  \mkleeneopen{}f  (\mlambda{}n.p)\mkleeneclose{}\mcdot{}

---

Home Index