proposition: Lemma update2_eq x u v w s : subs (update x v (update x w s)) u = subs (update x v s) u.
proof: Proof. apply subs_seq. intros z hz. unfold Def.update. eq_dec z x; refl. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)