---

Step * 2 of Lemma fps-rng_wf

.....set predicate..... 
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
⊢ Comm(|fps-rng(r)|;*)
BY
{ (RepUR ``fps-rng`` 0 THEN (D 0 THEN Auto) THEN Reduce 0 THEN BLemma `fps-mul-comm` THEN Auto) }

---

Latex:

---

Latex:
.....set  predicate..... 
1.  X  :  Type
2.  valueall-type(X)
3.  eq  :  EqDecider(X)
4.  r  :  CRng
\mvdash{}  Comm(|fps-rng(r)|;*)


By

---

Latex:
(RepUR  ``fps-rng``  0  THEN  (D  0  THEN  Auto)  THEN  Reduce  0  THEN  BLemma  `fps-mul-comm`  THEN  Auto)

---

Home Index