proposition: Lemma update2_neq_com s x u y v w : x <> y -> subs (update x u (update y v s)) w = subs (update y v (update x u s)) w.
proof: Proof. intro n. apply subs_seq. intros z hz. unfold Def.update. eq_dec z x; eq_dec z y; try refl. subst. tauto. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)