Step
*
2
of Lemma
Girard-theorem
.....wf..... 
istype(Type ∈ Type)
BY
{ Auto }
Latex:
Latex:
.....wf..... 
istype(Type  \mmember{}  Type)
By
Latex:
Auto
Home
Index