---

Step * 1 of Lemma Girard-theorem


1. Type ∈ Type
⊢ False
BY
{ TACTIC:(Assert WFO{i:l}() ∈ Type BY
                (Unfold `WFO` 0 THEN MemCD THEN Auto)) }

1
1. Type ∈ Type
2. WFO{i:l}() ∈ Type
⊢ False

---

Latex:

---

Latex:

1.  Type  \mmember{}  Type
\mvdash{}  False


By

---

Latex:
TACTIC:(Assert  WFO\{i:l\}()  \mmember{}  Type  BY
                            (Unfold  `WFO`  0  THEN  MemCD  THEN  Auto))

---

Home Index