---

Step * of Lemma compat-iff-common-iseg

∀[T:Type]. ∀l1,l2:T List.  (l1 || l2 ⇐⇒ ∃l:T List. (l1 ≤ l ∧ l2 ≤ l))
BY
{ Auto }

1
1. [T] : Type
2. l1 : T List@i
3. l2 : T List@i
4. l1 || l2@i
⊢ ∃l:T List. (l1 ≤ l ∧ l2 ≤ l)

2
1. [T] : Type
2. l1 : T List@i
3. l2 : T List@i
4. ∃l:T List. (l1 ≤ l ∧ l2 ≤ l)@i
⊢ l1 || l2

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index