Step
*
1
of Lemma
sorted-by-cons
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. x : T
4. L : T List
5. ∀i:ℕ||L|| + 1. ∀j:ℕi. (R [x / L][j] [x / L][i])
6. i : ℕ||L||
7. j : ℕi
⊢ R L[j] L[i]
BY
{ (((InstHyp [⌜i + 1⌝; ⌜j + 1⌝] (-3))⋅ THENA Auto) THEN (RWO "select_cons_tl" (-1)) THEN Auto) }
Latex:
Latex:
1. [T] : Type
2. [R] : T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}
3. x : T
4. L : T List
5. \mforall{}i:\mBbbN{}||L|| + 1. \mforall{}j:\mBbbN{}i. (R [x / L][j] [x / L][i])
6. i : \mBbbN{}||L||
7. j : \mBbbN{}i
\mvdash{} R L[j] L[i]
By
Latex:
(((InstHyp [\mkleeneopen{}i + 1\mkleeneclose{}; \mkleeneopen{}j + 1\mkleeneclose{}] (-3))\mcdot{} THENA Auto) THEN (RWO "select\_cons\_tl" (-1)) THEN Auto)
Home
Index