Step * 2 of Lemma Girard-theorem

.....wf..... 
istype(Type ∈ Type)
BY
Auto }


Latex:


Latex:
.....wf..... 
istype(Type  \mmember{}  Type)


By


Latex:
Auto




Home Index