---

Step * of Lemma remove-first-cons

∀[L,x,P:Top].  (remove-first(P;[x / L]) ~ if P x then L else [x / remove-first(P;L)] fi )
BY
{ ((UnivCD THENA Auto) THEN UnfoldAtAddr [1] 0 THEN Reduce 0 THEN Unfold `remove-first` 0 THEN EqCD) }

---

Latex:

---

Latex:
\mforall{}[L,x,P:Top].    (remove-first(P;[x  /  L])  \msim{}  if  P  x  then  L  else  [x  /  remove-first(P;L)]  fi  )


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  UnfoldAtAddr  [1]  0  THEN  Reduce  0  THEN  Unfold  `remove-first`  0  THEN  EqCD)

---

Home Index