---

Step * 1 1 2 2 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. v order-type-less() v
6. ¬(∀i:ℕ. (v order-type-less() v))
⊢ False
BY
{ TACTIC:(RenameVar `f' (-1) THEN RenameVar `p' (-2)) }

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))
⊢ 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.  v  order-type-less()  v
6.  \mneg{}(\mforall{}i:\mBbbN{}.  (v  order-type-less()  v))
\mvdash{}  False


By

---

Latex:
TACTIC:(RenameVar  `f'  (-1)  THEN  RenameVar  `p'  (-2))

---

Home Index