proposition: Lemma update_neq x u s y : x <> y -> update x u s y = s y.
proof: Proof. intro n. unfold Def.update. eq_dec y x. subst y. tauto. refl. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)