---

Step * 1 1 of Lemma Girard-theorem


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

1
.....assertion..... 
1. Type ∈ Type
2. WFO{i:l}() ∈ Type
⊢ max-WO{i:l}() ∈ WFO{i:l}()

2
1. Type ∈ Type
2. WFO{i:l}() ∈ Type
3. max-WO{i:l}() ∈ WFO{i:l}()
⊢ False

---

Latex:

---

Latex:

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


By

---

Latex:
TACTIC:Assert  \mkleeneopen{}max-WO\{i:l\}()  \mmember{}  WFO\{i:l\}()\mkleeneclose{}\mcdot{}

---

Home Index