---

Step * of Lemma diff_cons_lemma

∀bs,b,as,s:Top.  (as - [b / bs] ~ (as \ b) - bs)
BY
{ ((UnivCD THENA Auto) THEN RW (AddrC [1] (RecUnfoldC `diff`)) 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}bs,b,as,s:Top.    (as  -  [b  /  bs]  \msim{}  (as  \mbackslash{}  b)  -  bs)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RW  (AddrC  [1]  (RecUnfoldC  `diff`))  0  THEN  Reduce  0  THEN  Auto)

---

Home Index