---

Step * 1 of Lemma filter_iseg2


1. [T] : Type
2. L1 : T List
3. P : {x:T| (x ∈ [])}  ⟶ 𝔹
4. L1 ≤ []
⊢ filter(P;L1) ≤ []
BY
{ ((RWO "iseg_nil" (-1) THENA Auto)
   THEN (RW assert_pushdownC (-1) THENA Auto)
   THEN (FLemma `sqequal-nil` [-1] THENA Auto)
   THEN HypSubst (-1) 0
   THEN Reduce 0
   THEN BLemma `nil_iseg`
   THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  L1  :  T  List
3.  P  :  \{x:T|  (x  \mmember{}  [])\}    {}\mrightarrow{}  \mBbbB{}
4.  L1  \mleq{}  []
\mvdash{}  filter(P;L1)  \mleq{}  []


By

---

Latex:
((RWO  "iseg\_nil"  (-1)  THENA  Auto)
  THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto)
  THEN  (FLemma  `sqequal-nil`  [-1]  THENA  Auto)
  THEN  HypSubst  (-1)  0
  THEN  Reduce  0
  THEN  BLemma  `nil\_iseg`
  THEN  Auto)

---

Home Index