---

Step * of Lemma proper-iseg-append-one

∀[T:Type]. ∀L1,L2:T List. ∀x:T.  (L1 < L2 @ [x] ⇐⇒ L1 ≤ L2)
BY
{ (Unfold `proper-iseg` 0 THEN Auto THEN Try ((BLemma `iseg_append` THEN Auto))) }

1
1. [T] : Type
2. L1 : T List
3. L2 : T List
4. x : T
5. L1 ≤ L2 @ [x]
6. ¬(L1 = (L2 @ [x]) ∈ (T List))
⊢ L1 ≤ L2

2
1. T : Type
2. L1 : T List
3. L2 : T List
4. x : T
5. L1 ≤ L2
⊢ ¬(L1 = (L2 @ [x]) ∈ (T List))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L1,L2:T  List.  \mforall{}x:T.    (L1  <  L2  @  [x]  \mLeftarrow{}{}\mRightarrow{}  L1  \mleq{}  L2)


By

---

Latex:
(Unfold  `proper-iseg`  0  THEN  Auto  THEN  Try  ((BLemma  `iseg\_append`  THEN  Auto)))

---

Home Index