---

Step * of Lemma regextfun_wf2

∀[T:Type]. ∀[f:T ⟶ Set{i:l}]. ∀[w:W(T;x.set-dom(f x))].  (regextfun(f;w) ∈ Set{i:l})
BY
{ (Intros THEN Unhide THEN WElim (-1) THEN RecUnfold `regextfun` 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[f:T  {}\mrightarrow{}  Set\{i:l\}].  \mforall{}[w:W(T;x.set-dom(f  x))].    (regextfun(f;w)  \mmember{}  Set\{i:l\})


By

---

Latex:
(Intros  THEN  Unhide  THEN  WElim  (-1)  THEN  RecUnfold  `regextfun`  0  THEN  Reduce  0  THEN  Auto)

---

Home Index