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