Step
*
1
1
2
of Lemma
iota_wf
.....eq aux.....
1. I : Cname List
2. x : Cname
⊢ nameset(I) ∈ Type
BY
{ Auto }
Latex:
Latex:
.....eq aux.....
1. I : Cname List
2. x : Cname
\mvdash{} nameset(I) \mmember{} Type
By
Latex:
Auto
Home
Index