proposition: Lemma read_over_same_write : forall a i j v, i = j -> select (store a i v) j = Some v.
proof: Proof. intros a i j v Heq. unfold select, store. intros. rewrite add_eq_o; auto. Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses