---

Step * of Lemma fset-extensionality

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x,y:fset(T)].  uiff(x = y ∈ fset(T);∀[a:T]. uiff(a ∈ x;a ∈ y))
BY
{ (Auto THEN Try ((NthHypEq (-1) THEN EqCD THEN Auto))) }

1
1. T : Type
2. eq : EqDecider(T)
3. x : fset(T)
4. y : fset(T)
5. ∀[a:T]. uiff(a ∈ x;a ∈ y)
⊢ x = y ∈ fset(T)

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  Try  ((NthHypEq  (-1)  THEN  EqCD  THEN  Auto)))

---

Home Index