Step
*
1
2
1
of Lemma
member-insert
.....equality.....
1. T : Type
2. eq : EqDecider(T)
3. a : T
4. L : T List
5. b : T
6. ¬(a ∈ L)
⊢ insert(a;L) ~ [a / L]
BY
{ BLemma `insert-cases`
THEN Auto⋅ }
Latex:
Latex:
.....equality.....
1. T : Type
2. eq : EqDecider(T)
3. a : T
4. L : T List
5. b : T
6. \mneg{}(a \mmember{} L)
\mvdash{} insert(a;L) \msim{} [a / L]
By
Latex:
BLemma `insert-cases`
THEN Auto\mcdot{}
Home
Index