Step
*
3
of Lemma
int_ring_wf
.....wf..... 
1. r : CRng
⊢ IsIntegDom(r) ∈ Type
BY
{ Auto }
Latex:
Latex:
.....wf..... 
1.  r  :  CRng
\mvdash{}  IsIntegDom(r)  \mmember{}  Type
By
Latex:
Auto
Home
Index