---

Step * of Lemma cosetTC_wf2

∀[a:Set{i:l}]. (cosetTC(a) ∈ Set{i:l})
BY
{ (Intro
   THEN RepUR ``cosetTC mk-coset`` 0
   THEN Fold `Wsup` 0
   THEN All (Unfold `Set`)
   THEN (Assert ⌜a ∈ coW(Type;x.x)⌝⋅ THENA Auto)
   THEN InstLemma `copath-at-W` [⌜Type⌝;⌜λ2x.x⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a:Set\{i:l\}].  (cosetTC(a)  \mmember{}  Set\{i:l\})


By

---

Latex:
(Intro
  THEN  RepUR  ``cosetTC  mk-coset``  0
  THEN  Fold  `Wsup`  0
  THEN  All  (Unfold  `Set`)
  THEN  (Assert  \mkleeneopen{}a  \mmember{}  coW(Type;x.x)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  InstLemma  `copath-at-W`  [\mkleeneopen{}Type\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.x\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index