---

Step * of Lemma W-select_wf

∀[A:Type]. ∀[B:A ⟶ Type]. ∀[s:(a:A ⟶ (B[a]?)) List]. ∀[w:co-W(A;a.B[a])].  (W-select(w;s) ∈ co-W(A;a.B[a])?)
BY
{ (InductionOnList
   THEN RecUnfold `W-select` 0
   THEN Reduce 0
   THEN Auto
   THEN co_WD (-1)
   THEN D -1
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[s:(a:A  {}\mrightarrow{}  (B[a]?))  List].  \mforall{}[w:co-W(A;a.B[a])].
    (W-select(w;s)  \mmember{}  co-W(A;a.B[a])?)


By

---

Latex:
(InductionOnList
  THEN  RecUnfold  `W-select`  0
  THEN  Reduce  0
  THEN  Auto
  THEN  co\_WD  (-1)
  THEN  D  -1
  THEN  Reduce  0
  THEN  Auto)

---

Home Index