proposition: Theorem set_compat : forall A x y v dom₁ dom₂ (m₁ : t A dom₁) (m₂ : t A dom₂) (Hin₁ : Dom.In x dom₁) (Hin₂ : Dom.In y dom₂), X.eq x y -> eq m₁ m₂ -> eq (set x v m₁ Hin₁) (set y v m₂ Hin₂).
proof: Proof. intros A x y v dom₁ dom₂ m₁ m₂ Hin₁ Hin₂ Hxy Hm z. destruct (X.eq_dec z x) as [Hxz | Hxz]. + rewrite Hxz. rewrite Hxy at 3. do 2 rewrite set_same. reflexivity. + repeat rewrite set_other; auto. rewrite <- Hxy. assumption. Qed.
imports: Utf8 Bool SetoidList RelationPairs Orders Coqlib DepMapInterface DepMapFactsInterface