---

Step * 1 1 1 of Lemma Girard-theorem

.....assertion..... 
1. Type ∈ Type
2. WFO{i:l}() ∈ Type
⊢ max-WO{i:l}() ∈ WFO{i:l}()
BY
{ TACTIC:(Unfold `WFO` 0⋅ THEN Unfold `max-WO` 0 THEN Auto THEN Unfold `WFO` 0 THEN ProveWfLemma) }

---

Latex:

---

Latex:
.....assertion..... 
1.  Type  \mmember{}  Type
2.  WFO\{i:l\}()  \mmember{}  Type
\mvdash{}  max-WO\{i:l\}()  \mmember{}  WFO\{i:l\}()


By

---

Latex:
TACTIC:(Unfold  `WFO`  0\mcdot{}  THEN  Unfold  `max-WO`  0  THEN  Auto  THEN  Unfold  `WFO`  0  THEN  ProveWfLemma)

---

Home Index