---

Step * of Lemma iseg_append_single

∀[T:Type]. ∀l1,l2:T List. ∀x:T.  (l1 ≤ l2 @ [x] ⇐⇒ l1 ≤ l2 ∨ (l1 = (l2 @ [x]) ∈ (T List)))
BY
{ ((UnivCD THENA Auto) THEN RWO "iseg_append_iff" 0 THEN Auto THEN ParallelLast THEN ExRepD) }

1
1. T : Type
2. l1 : T List
3. l2 : T List
4. x : T
5. l : T List
6. 0 < ||l||
7. l1 = (l2 @ l) ∈ (T List)
8. l ≤ [x]
⊢ l1 = (l2 @ [x]) ∈ (T List)

2
1. [T] : Type
2. l1 : T List
3. l2 : T List
4. x : T
5. l1 = (l2 @ [x]) ∈ (T List)
⊢ ∃l:T List. (0 < ||l|| ∧ (l1 = (l2 @ l) ∈ (T List)) ∧ l ≤ [x])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}l1,l2:T  List.  \mforall{}x:T.    (l1  \mleq{}  l2  @  [x]  \mLeftarrow{}{}\mRightarrow{}  l1  \mleq{}  l2  \mvee{}  (l1  =  (l2  @  [x])))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RWO  "iseg\_append\_iff"  0  THEN  Auto  THEN  ParallelLast  THEN  ExRepD)

---

Home Index