proposition: Lemma subs1_update2_single_eq y w x v v' u : subs1 (update y w (update x v' (single x v))) u = subs1 (update y w (single x v')) u.
proof: Proof. apply subs1_seq. intros z hz. unfold Def.update at -2. eq_dec z y. refl. match goal with |- ?x _ = ?y _ => set (s1:=x); set (s2:=y) end. change (subs s1 (Var z) = subs s2 (Var z)). unfold s1, s2. rewrite update_single_eq. refl. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)