---

Step * 1 of Lemma accum_filter_rel_wf

.....assertion..... 
1. T : Type
2. A : Type
3. a : A
4. b : A
5. X : T List
6. P : {x:T| (x ∈ X)}  ⟶ ℙ
7. f : A ⟶ {x:T| (x ∈ X)}  ⟶ A
8. L : T List@i
9. L ⊆ X c∧ (∀x:T. ((x ∈ L) ⇐⇒ (x ∈ X) c∧ P[x]))
⊢ L ∈ {x:T| (x ∈ X)}  List
BY
{ (((InstLemma `list-subtype` [⌜T⌝; ⌜L⌝])⋅ THENA Auto) THEN DoSubsume THEN Auto THEN SubtypeReasoning THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  T  :  Type
2.  A  :  Type
3.  a  :  A
4.  b  :  A
5.  X  :  T  List
6.  P  :  \{x:T|  (x  \mmember{}  X)\}    {}\mrightarrow{}  \mBbbP{}
7.  f  :  A  {}\mrightarrow{}  \{x:T|  (x  \mmember{}  X)\}    {}\mrightarrow{}  A
8.  L  :  T  List@i
9.  L  \msubseteq{}  X  c\mwedge{}  (\mforall{}x:T.  ((x  \mmember{}  L)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  X)  c\mwedge{}  P[x]))
\mvdash{}  L  \mmember{}  \{x:T|  (x  \mmember{}  X)\}    List


By

---

Latex:
(((InstLemma  `list-subtype`  [\mkleeneopen{}T\mkleeneclose{};  \mkleeneopen{}L\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  DoSubsume
  THEN  Auto
  THEN  SubtypeReasoning
  THEN  Auto)

---

Home Index