---

Step * 1 1 of Lemma l_before_append_iff


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
BY
{ TACTIC:(SplitOrHyps 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

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  B  :  T  List@i
3.  x  :  T@i
4.  y  :  T@i
5.  x  before  y  \mmember{}  []  \mvee{}  x  before  y  \mmember{}  B  \mvee{}  ((x  \mmember{}  [])  \mwedge{}  (y  \mmember{}  B))
\mvdash{}  x  before  y  \mmember{}  B


By

---

Latex:
TACTIC:(SplitOrHyps  THEN  Auto)

---

Home Index