proposition: Lemma subs1_update_single_eq y v w u : subs1 (update y w (single y v)) u = subs1 (single y w) u.
proof: Proof. apply subs1_seq. intros b hb. unfold Def.single, Def.update. eq_dec b y; refl. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)