---

Step * of Lemma Wselect_wf

∀[A:Type]
  ∀[B:A ⟶ Type]. ∀[s:(a:A ⟶ (B[a]?)) List]. ∀[w:W-type(A; a.B[a])].  (Wselect(w;s) ∈ W-type(A; a.B[a])?) 
  supposing ∀x,y:A.  Dec(x = y ∈ A)
BY
{ xxx(Unfold `Wselect` 0
      THEN InductionOnList
      THEN RecUnfold `W-select` 0
      THEN Reduce 0
      THEN Try (Complete (Auto))
      THEN (UnivCD THENA Auto)
      THEN WD (-1)
      THEN Reduce 0
      THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[A:Type]
    \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[s:(a:A  {}\mrightarrow{}  (B[a]?))  List].  \mforall{}[w:W-type(A;  a.B[a])].
        (Wselect(w;s)  \mmember{}  W-type(A;  a.B[a])?) 
    supposing  \mforall{}x,y:A.    Dec(x  =  y)


By

---

Latex:
xxx(Unfold  `Wselect`  0
        THEN  InductionOnList
        THEN  RecUnfold  `W-select`  0
        THEN  Reduce  0
        THEN  Try  (Complete  (Auto))
        THEN  (UnivCD  THENA  Auto)
        THEN  WD  (-1)
        THEN  Reduce  0
        THEN  Auto)xxx

---

Home Index