Commit 7246cee7 authored by Robbert Krebbers's avatar Robbert Krebbers

CMRA structure on lists.

Initial commit by Amin Timany.
parent 2e67e68f
......@@ -983,6 +983,11 @@ Proof.
- intros [-> Hi]. revert i Hi.
induction n; intros [|?]; naive_solver auto with lia.
Lemma elem_of_replicate n x y : y ∈ replicate n x ↔ y = x ∧ n ≠ 0.
rewrite elem_of_list_lookup, Nat.neq_0_lt_0.
setoid_rewrite lookup_replicate; naive_solver eauto with lia.
Lemma lookup_replicate_1 n x y i :
replicate n x !! i = Some y → y = x ∧ i < n.
Proof. by rewrite lookup_replicate. Qed.
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