---

Step * of Lemma common_iseg_compat

∀[T:Type]. ∀l,l1,l2:T List.  (l1 ≤ l ⇒ l2 ≤ l ⇒ l1 || l2)
BY
{ (RepeatFor 4 (Intro) THEN ((Unfold `compat` 0 THEN RWW "iseg_select" 0) THEN Auto) THEN ExRepD) }

1
1. [T] : Type
2. l : T List
3. l1 : T List
4. l2 : T List
5. ||l1|| ≤ ||l||
6. ∀i:ℕ. l1[i] = l[i] ∈ T supposing i < ||l1||
7. ||l2|| ≤ ||l||
8. ∀i:ℕ. l2[i] = l[i] ∈ T supposing i < ||l2||
⊢ ((||l1|| ≤ ||l2||) c∧ (∀i:ℕ. l1[i] = l2[i] ∈ T supposing i < ||l1||))
∨ ((||l2|| ≤ ||l1||) c∧ (∀i:ℕ. l2[i] = l1[i] ∈ T supposing i < ||l2||))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}l,l1,l2:T  List.    (l1  \mleq{}  l  {}\mRightarrow{}  l2  \mleq{}  l  {}\mRightarrow{}  l1  ||  l2)


By

---

Latex:
(RepeatFor  4  (Intro)  THEN  ((Unfold  `compat`  0  THEN  RWW  "iseg\_select"  0)  THEN  Auto)  THEN  ExRepD)

---

Home Index