Commit 3bffafaa authored by Ralf Jung's avatar Ralf Jung
Browse files

tweaks

parent 18ce1146
Pipeline #47073 passed with stage
in 4 minutes and 55 seconds
......@@ -598,9 +598,9 @@ Lemma lookup_cons x l i :
Proof. reflexivity. Qed.
Lemma lookup_cons_Some x l i y :
(x :: l) !! i = Some y
(x = y i = 0) (1 i l !! (i - 1) = Some y).
(i = 0 x = y) (1 i l !! (i - 1) = Some y).
Proof.
rewrite lookup_cons. destruct i.
rewrite lookup_cons. destruct i as [|i].
- naive_solver lia.
- replace (S i - 1) with i by lia. naive_solver lia.
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