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