proposition: Lemma read_over_other_write : forall a i j v, i <> j -> select (store a i v) j = select a j.
proof: Proof. intros a i j v Hneq. unfold select, store. apply (add_neq_o a v) in Hneq. rewrite Hneq. auto. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance