---

Step * of Lemma Girard-theorem

¬(Type ∈ Type)
BY
{ D 0⋅ }

1
1. Type ∈ Type
⊢ False

2
.....wf..... 
istype(Type ∈ Type)

---

Latex:

---

Latex:
\mneg{}(Type  \mmember{}  Type)


By

---

Latex:
D  0\mcdot{}

---

Home Index