---

Step * of Lemma l_before_filter_subtype

∀[T:Type]
  ∀l:T List. ∀P:T ⟶ 𝔹. ∀x,y:T.  ((↑(P x)) ⇒ (↑(P y)) ⇒ (x before y ∈ filter(P;l) ⇐⇒ x before y ∈ filter(P;l)))
BY
{ (TACTIC:Auto
   THEN All(Unfold `l_before`)
   THEN All(Unfold `sublist`)
   THEN AllReduce
   THEN ParallelLast
   THEN Auto
   THEN IntSegCases (-1)
   THEN Reduce 0
   THEN Try (Complete ((RWO "10<" 0 THEN Auto)))) }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}l:T  List.  \mforall{}P:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}x,y:T.
        ((\muparrow{}(P  x))  {}\mRightarrow{}  (\muparrow{}(P  y))  {}\mRightarrow{}  (x  before  y  \mmember{}  filter(P;l)  \mLeftarrow{}{}\mRightarrow{}  x  before  y  \mmember{}  filter(P;l)))


By

---

Latex:
(TACTIC:Auto
  THEN  All(Unfold  `l\_before`)
  THEN  All(Unfold  `sublist`)
  THEN  AllReduce
  THEN  ParallelLast
  THEN  Auto
  THEN  IntSegCases  (-1)
  THEN  Reduce  0
  THEN  Try  (Complete  ((RWO  "10<"  0  THEN  Auto))))

---

Home Index