---

Step * of Lemma isSet_functionality

∀a1,a2:coSet{i:l}.  (seteq(a1;a2) ⇒ (isSet(a1) ⇐⇒ isSet(a2)))
BY
{ (All (RepUR ``coSet isSet seteq``) THEN InstLemma `coW-wfdd_functionality` [⌜Type⌝;⌜λ2x.x⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}a1,a2:coSet\{i:l\}.    (seteq(a1;a2)  {}\mRightarrow{}  (isSet(a1)  \mLeftarrow{}{}\mRightarrow{}  isSet(a2)))


By

---

Latex:
(All  (RepUR  ``coSet  isSet  seteq``)
  THEN  InstLemma  `coW-wfdd\_functionality`  [\mkleeneopen{}Type\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.x\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index