∀[r:CRng]. Comm(|r|;*)
{ D 0 THENA Auto }
1. r : CRng
⊢ Comm(|r|;*)