---

Step * of Lemma list-to-set-cons

∀[T:Type]
  ∀eq:EqDecider(T). ∀L:T List. ∀a:T.
    (list-to-set(eq;[a / L]) ~ if a ∈b list-to-set(eq;L) then list-to-set(eq;L) else [a / list-to-set(eq;L)] fi )
BY
{ ((UnivCD THENA Auto)
   THEN (RW (AddrC [1] (UnfoldTopAbC)) 0 THEN RepUR ``l-union insert`` 0)
   THEN RWO "eval_list_sq" 0
   THEN Fold `insert` 0
   THEN Try (Complete (Auto))
   THEN Fold `l-union` 0
   THEN Fold `list-to-set` 0
   THEN CallByValueReduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T).  \mforall{}L:T  List.  \mforall{}a:T.
        (list-to-set(eq;[a  /  L])  \msim{}  if  a  \mmember{}\msubb{}  list-to-set(eq;L)
        then  list-to-set(eq;L)
        else  [a  /  list-to-set(eq;L)]
        fi  )


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (RW  (AddrC  [1]  (UnfoldTopAbC))  0  THEN  RepUR  ``l-union  insert``  0)
  THEN  RWO  "eval\_list\_sq"  0
  THEN  Fold  `insert`  0
  THEN  Try  (Complete  (Auto))
  THEN  Fold  `l-union`  0
  THEN  Fold  `list-to-set`  0
  THEN  CallByValueReduce  0
  THEN  Auto)

---

Home Index