---

Step * of Lemma assert_of_rng_eq

∀[r:DRng]. ∀[a,b:|r|].  uiff(↑(a =b b);a = b ∈ |r|)
BY
{ ((Fold `eqfun_p` 0 THENM RepD  
THENM OnVar `r' AddAllProperties) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[r:DRng].  \mforall{}[a,b:|r|].    uiff(\muparrow{}(a  =\msubb{}  b);a  =  b)


By

---

Latex:
((Fold  `eqfun\_p`  0  THENM  RepD   
THENM  OnVar  `r'  AddAllProperties)  THEN  Auto)

---

Home Index