---

Step * of Lemma cons_iseg

∀[T:Type]. ∀a,b:T. ∀l1,l2:T List.  ([a / l1] ≤ [b / l2] ⇐⇒ (a = b ∈ T) ∧ l1 ≤ l2)
BY
{ ((Unfold `iseg` 0 THEN Auto) THEN ExRepD) }

1
1. T : Type
2. a : T
3. b : T
4. l1 : T List
5. l2 : T List
6. l : T List
7. [b / l2] = ([a / l1] @ l) ∈ (T List)
⊢ a = b ∈ T

2
1. [T] : Type
2. a : T
3. b : T
4. l1 : T List
5. l2 : T List
6. l : T List
7. [b / l2] = ([a / l1] @ l) ∈ (T List)
⊢ ∃l:T List. (l2 = (l1 @ l) ∈ (T List))

3
1. [T] : Type
2. a : T
3. b : T
4. l1 : T List
5. l2 : T List
6. a = b ∈ T
7. l : T List
8. l2 = (l1 @ l) ∈ (T List)
⊢ ∃l:T List. ([b / l2] = ([a / l1] @ l) ∈ (T List))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}a,b:T.  \mforall{}l1,l2:T  List.    ([a  /  l1]  \mleq{}  [b  /  l2]  \mLeftarrow{}{}\mRightarrow{}  (a  =  b)  \mwedge{}  l1  \mleq{}  l2)


By

---

Latex:
((Unfold  `iseg`  0  THEN  Auto)  THEN  ExRepD)

---

Home Index