Commit bffad30d authored by Amin Timany's avatar Amin Timany
Browse files

Add property about altering singleton lists

parent 229f2dba
......@@ -556,6 +556,15 @@ Section properties.
* apply IHj; eauto.
inversion Hm; trivial.
Qed.
(* altering a singleton is just altering the underlying element. *)
Lemma list_alter_singleton `{CMRAUnit A} {L : A A} i x :
alter L i {[i := x]} = {[i := L x]}.
Proof.
induction i; simpl; trivial.
apply (f_equal (cons _)); simpl; trivial.
Qed.
End properties.
(** Functor *)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment