proposition: Lemma update_single_eq y v w u : subs (update y w (single y v)) u = subs (single y w) u.
proof: Proof. unfold Def.single at 1. rewrite update2_eq. refl. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)