---

Step * of Lemma iseg-append-one

∀[T:Type]. ∀L1,L2:T List. ∀x:T.  (L1 ≤ L2 @ [x] ⇐⇒ L1 ≤ L2 ∨ (L1 = (L2 @ [x]) ∈ (T List)))
BY
{ Auto }

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

2
1. [T] : Type
2. L1 : T List
3. L2 : T List
4. x : T
5. L1 ≤ L2 ∨ (L1 = (L2 @ [x]) ∈ (T List))
⊢ L1 ≤ L2 @ [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:
Auto

---

Home Index