---

Step * 1 of Lemma l_before_append_iff


1. [T] : Type
⊢ ∀B:T List. ∀x,y:T.  (x before y ∈ [] @ B ⇐⇒ x before y ∈ [] ∨ x before y ∈ B ∨ ((x ∈ []) ∧ (y ∈ B)))
BY
{ TACTIC:(Reduce 0 THEN Auto) }

1
1. [T] : Type
2. B : T List@i
3. x : T@i
4. y : T@i
5. x before y ∈ [] ∨ x before y ∈ B ∨ ((x ∈ []) ∧ (y ∈ B))
⊢ x before y ∈ B

---

Latex:

---

Latex:

1.  [T]  :  Type
\mvdash{}  \mforall{}B:T  List.  \mforall{}x,y:T.
        (x  before  y  \mmember{}  []  @  B  \mLeftarrow{}{}\mRightarrow{}  x  before  y  \mmember{}  []  \mvee{}  x  before  y  \mmember{}  B  \mvee{}  ((x  \mmember{}  [])  \mwedge{}  (y  \mmember{}  B)))


By

---

Latex:
TACTIC:(Reduce  0  THEN  Auto)

---

Home Index