---

Step * of Lemma regextW_wf

∀[T:Type]. ∀[f:T ⟶ coSet{i:l}]. ∀[G:i:T ⟶ j:set-dom(f i) ⟶ T]. ∀[t:T].  (regextW(G;t) ∈ coW(T;x.set-dom(f x)))
BY
{ (Auto THEN Unfold `regextW` 0 THEN (BLemma `fix_wf_coW_parameter` THEN Auto) THEN Unfold `Wsup` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[f:T  {}\mrightarrow{}  coSet\{i:l\}].  \mforall{}[G:i:T  {}\mrightarrow{}  j:set-dom(f  i)  {}\mrightarrow{}  T].  \mforall{}[t:T].
    (regextW(G;t)  \mmember{}  coW(T;x.set-dom(f  x)))


By

---

Latex:
(Auto
  THEN  Unfold  `regextW`  0
  THEN  (BLemma  `fix\_wf\_coW\_parameter`  THEN  Auto)
  THEN  Unfold  `Wsup`  0
  THEN  Auto)

---

Home Index