---

Step * 1 of Lemma filter_before


1. [A] : Type
⊢ ∀P:A ⟶ 𝔹. ∀x,y:A.  (x before y ∈ [] ⇐⇒ (↑(P x)) ∧ (↑(P y)) ∧ x before y ∈ [])
BY
{ ((RWO "nil_before" 0 THENA Auto) THEN SimpConcl) }

---

Latex:

---

Latex:

1.  [A]  :  Type
\mvdash{}  \mforall{}P:A  {}\mrightarrow{}  \mBbbB{}.  \mforall{}x,y:A.    (x  before  y  \mmember{}  []  \mLeftarrow{}{}\mRightarrow{}  (\muparrow{}(P  x))  \mwedge{}  (\muparrow{}(P  y))  \mwedge{}  x  before  y  \mmember{}  [])


By

---

Latex:
((RWO  "nil\_before"  0  THENA  Auto)  THEN  SimpConcl)

---

Home Index