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` THEN Auto) THEN ExRepD) }

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

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

3
1. [T] Type
2. T
3. T
4. l1 List
5. l2 List
6. b ∈ T
7. 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