---

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

.....wf..... 
1. Type ∈ Type
2. WFO{i:l}() ∈ Type
3. trans : max-WO{i:l}() ∈ WFO{i:l}()
⊢ max-WFTO{i:l}() ∈ WFTRO{i:l}()
BY
{ ((Unfold `WFTRO` 0 THEN Unfold `max-WFTO` 0) THEN Auto THEN Unfold `WFO` 0 THEN ProveWfLemma) }

---

Latex:

---

Latex:
.....wf..... 
1.  Type  \mmember{}  Type
2.  WFO\{i:l\}()  \mmember{}  Type
3.  trans  :  max-WO\{i:l\}()  \mmember{}  WFO\{i:l\}()
\mvdash{}  max-WFTO\{i:l\}()  \mmember{}  WFTRO\{i:l\}()


By

---

Latex:
((Unfold  `WFTRO`  0  THEN  Unfold  `max-WFTO`  0)  THEN  Auto  THEN  Unfold  `WFO`  0  THEN  ProveWfLemma)

---

Home Index