proposition: Lemma read_over_same_write : forall a i j v, i = j -> select (store a i v) j = v.
proof: Proof. intros a i j v Heq. unfold select, store. case_eq (cmp v default_value); intro H; auto. - unfold cmp, compare2eqb in H. case (compare v default_value) as [ | |e] in H; auto; try now contradict H. rewrite e. rewrite add_eq_d; auto. - assert (H0: v <> default_value). { unfold cmp, compare2eqb in H. case (compare v default_value) as [l|e|l] in H; auto; try now contradict H. - apply lt_not_eq in l. auto. - apply lt_not_eq in l. auto. } rewrite (add_eq_o a Heq H0). auto. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance