---

Step * of Lemma member-fset-singleton

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x,y:T].  uiff(y ∈ {x};y = x ∈ T)
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``fset-member fset-singleton eqof`` 0
   THEN (RW assert_pushdownC 0 THENA Auto)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[x,y:T].    uiff(y  \mmember{}  \{x\};y  =  x)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``fset-member  fset-singleton  eqof``  0
  THEN  (RW  assert\_pushdownC  0  THENA  Auto)
  THEN  Auto)

---

Home Index