---

Step * of Lemma co-seteq-iff

∀x,y:coSet{i:l}.  (seteq(x;y) ⇐⇒ ∀z:coSet{i:l}. ((z ∈ x) ⇐⇒ (z ∈ y)))
BY
{ ((InstLemma `coW-equiv-iff` [⌜Type⌝;⌜λ2T.T⌝]⋅ THENA Auto) THEN Folds ``seteq setmem coSet`` (-1) THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}x,y:coSet\{i:l\}.    (seteq(x;y)  \mLeftarrow{}{}\mRightarrow{}  \mforall{}z:coSet\{i:l\}.  ((z  \mmember{}  x)  \mLeftarrow{}{}\mRightarrow{}  (z  \mmember{}  y)))


By

---

Latex:
((InstLemma  `coW-equiv-iff`  [\mkleeneopen{}Type\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}T.T\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Folds  ``seteq  setmem  coSet``  (-1)
  THEN  Trivial)

---

Home Index