---

Step * of Lemma l-ordered-cons

∀[T:Type]
  ∀x:T. ∀L:T List.
    ∀[R:T ⟶ T ⟶ ℙ]. (l-ordered(T;x,y.R[x;y];[x / L]) ⇐⇒ l-ordered(T;x,y.R[x;y];L) ∧ (∀y:T. ((y ∈ L) ⇒ R[x;y])))
BY
{ Auto }

1
1. [T] : Type
2. x : T
3. L : T List
4. [R] : T ⟶ T ⟶ ℙ
5. l-ordered(T;x,y.R[x;y];[x / L])
⊢ l-ordered(T;x,y.R[x;y];L)

2
1. [T] : Type
2. x : T
3. L : T List
4. [R] : T ⟶ T ⟶ ℙ
5. l-ordered(T;x,y.R[x;y];[x / L])
6. y : T
7. (y ∈ L)
⊢ R[x;y]

3
1. [T] : Type
2. x : T
3. L : T List
4. [R] : T ⟶ T ⟶ ℙ
5. l-ordered(T;x,y.R[x;y];L)
6. ∀y:T. ((y ∈ L) ⇒ R[x;y])
⊢ l-ordered(T;x,y.R[x;y];[x / L])

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}x:T.  \mforall{}L:T  List.
        \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}]
            (l-ordered(T;x,y.R[x;y];[x  /  L])  \mLeftarrow{}{}\mRightarrow{}  l-ordered(T;x,y.R[x;y];L)  \mwedge{}  (\mforall{}y:T.  ((y  \mmember{}  L)  {}\mRightarrow{}  R[x;y])))


By

---

Latex:
Auto

---

Home Index