---

Step * 2 of Lemma compat-iff-common-iseg


1. [T] : Type
2. l1 : T List@i
3. l2 : T List@i
4. ∃l:T List. (l1 ≤ l ∧ l2 ≤ l)@i
⊢ l1 || l2
BY
{ (ExRepD THEN (Using [`l',⌜l⌝] (BLemma `common_iseg_compat`))⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  l1  :  T  List@i
3.  l2  :  T  List@i
4.  \mexists{}l:T  List.  (l1  \mleq{}  l  \mwedge{}  l2  \mleq{}  l)@i
\mvdash{}  l1  ||  l2


By

---

Latex:
(ExRepD  THEN  (Using  [`l',\mkleeneopen{}l\mkleeneclose{}]  (BLemma  `common\_iseg\_compat`))\mcdot{}  THEN  Auto)

---

Home Index