---

Step * of Lemma remove1_cons_lemma

∀bs,b,a,s:Top.  ([b / bs] \ a ~ if b (=b) a then bs else [b / (bs \ a)] fi )
BY
{ ((UnivCD THENA Auto) THEN (RW (AddrC [1] (RecUnfoldC `remove1`))) 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}bs,b,a,s:Top.    ([b  /  bs]  \mbackslash{}  a  \msim{}  if  b  (=\msubb{})  a  then  bs  else  [b  /  (bs  \mbackslash{}  a)]  fi  )


By

---

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

---

Home Index