---

Step * of Lemma remove-repeats-normal-form

∀[eq,L:Top].
  (rec-case(L) of
   [] => []
   a::_ =>
    r.[a / rec-case(r) of [] => [] | a@0::_ => r.if eq a@0 a then r else [a@0 / r] fi ] ~ remove-repeats(eq;L))
BY
{ (UnivCD THENA Auto)
THEN (SymbComp 0 THEN Auto) }

---

Latex:


\mforall{}[eq,L:Top].
    (rec-case(L)  of
      []  =>  []
      a::$_{}$  =>
        r.[a  /  rec-case(r)  of  []  =>  []  |  a@0::$_{}$  =>  r.if  eq  a@0  a  then  r  else  [a@\000C0  /  r]  fi  ] 
    \msim{}  remove-repeats(eq;L))


By

(UnivCD  THENA  Auto)
THEN  (SymbComp  0  THEN  Auto)

---

Home Index