---

Step * of Lemma mapfilter-wf

∀[T,U:Type]. ∀[L:T List]. ∀[P:T ⟶ 𝔹]. ∀[f:{x:T| (x ∈ L) ∧ (↑P[x])}  ⟶ U].  (mapfilter(f;P;L) ∈ U List)
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `mapfilter` 0
   THEN Using [`A',⌜{x:T| (x ∈ L) ∧ (↑P[x])} ⌝] (BLemma `map_wf`)⋅
   THEN Try (Complete (Auto))
   THEN (InstLemma `filter_wf4_2` [⌜T⌝;⌜P⌝;⌜L⌝]⋅ THEN Auto)) }

---

Latex:

---

Latex:
\mforall{}[T,U:Type].  \mforall{}[L:T  List].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[f:\{x:T|  (x  \mmember{}  L)  \mwedge{}  (\muparrow{}P[x])\}    {}\mrightarrow{}  U].
    (mapfilter(f;P;L)  \mmember{}  U  List)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `mapfilter`  0
  THEN  Using  [`A',\mkleeneopen{}\{x:T|  (x  \mmember{}  L)  \mwedge{}  (\muparrow{}P[x])\}  \mkleeneclose{}]  (BLemma  `map\_wf`)\mcdot{}
  THEN  Try  (Complete  (Auto))
  THEN  (InstLemma  `filter\_wf4\_2`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THEN  Auto))

---

Home Index