proposition: Theorem add_merge : forall A x v₁ v₂ dom (m : t A dom), eq (add x v₂ (add x v₁ m)) (add x v₂ m).
proof: Proof. intros A x v₁ v₂ dom m y. destruct (X.eq_dec y x) as [Hxy | Hxy]. + rewrite Hxy, add_same, add_same. reflexivity. + repeat rewrite add_other; trivial. Qed.
imports: Utf8 Bool SetoidList RelationPairs Orders Coqlib DepMapInterface DepMapFactsInterface