Commit 213f085b authored by Hai Dang's avatar Hai Dang
Browse files

minor cleanup

parent d6c72828
......@@ -15,11 +15,6 @@ From gpfsl.examples.exchanger Require Import spec_graph spec_graph_piggyback.
Require Import iris.prelude.options.
(* TODO: move *)
Lemma lookup_length_not_Some {A} (l : list A) (x : A) : ¬ l !! length l = Some x.
Proof. rewrite lookup_ge_None_2; [done|lia]. Qed.
Lemma lookup_length_not_is_Some {A} (l : list A) : ¬ is_Some (l !! length l).
Proof. by intros [? ?%lookup_length_not_Some]. Qed.
Lemma sum_relation_impl {A B} (RA RA' : relation A) (RB RB': relation B) :
ab1 ab2,
( a1 a2, ab1 = inl a1 ab2 = inl a2 RA a1 a2 RA' a1 a2)
Supports Markdown
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