---

Step * of Lemma filter_fseg

∀[T:Type]. ∀P:T ⟶ 𝔹. ∀L2,L1:T List.  (fseg(T;L1;L2) ⇒ fseg(T;filter(P;L1);filter(P;L2)))
BY
{ (((Auto THEN ParallelLast) THEN ExRepD)
   THEN (HypSubst' -1 0 THENA Auto)
   THEN (InstConcl [⌜filter(P;L)⌝]⋅ THEN Auto)
   THEN RWO "filter_append" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}P:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}L2,L1:T  List.    (fseg(T;L1;L2)  {}\mRightarrow{}  fseg(T;filter(P;L1);filter(P;L2)))


By

---

Latex:
(((Auto  THEN  ParallelLast)  THEN  ExRepD)
  THEN  (HypSubst'  -1  0  THENA  Auto)
  THEN  (InstConcl  [\mkleeneopen{}filter(P;L)\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  RWO  "filter\_append"  0
  THEN  Auto)

---

Home Index