Step
*
1
of Lemma
l_all2_cons
1. [T] : Type
2. L : T List
3. [P] : T ⟶ T ⟶ ℙ
4. u : T
5. ∀y:T. ((y ∈ L)
⇒ P[u;y])
6. ∀x,y:T. (x before y ∈ L
⇒ P[x;y])
7. x : T
8. y : T
9. ((x = u ∈ T) ∧ (y ∈ L)) ∨ x before y ∈ L
⊢ P[x;y]
BY
{ (D (-1) THEN Auto) }
Latex:
Latex:
1. [T] : Type
2. L : T List
3. [P] : T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}
4. u : T
5. \mforall{}y:T. ((y \mmember{} L) {}\mRightarrow{} P[u;y])
6. \mforall{}x,y:T. (x before y \mmember{} L {}\mRightarrow{} P[x;y])
7. x : T
8. y : T
9. ((x = u) \mwedge{} (y \mmember{} L)) \mvee{} x before y \mmember{} L
\mvdash{} P[x;y]
By
Latex:
(D (-1) THEN Auto)
Home
Index