proposition: Lemma update_id x s u : s x = Var x -> subs (update x (Var x) s) u = subs s u.
proof: Proof. intro h. apply subs_seq. intros z hz. unfold Def.update. eq_dec z x. subst. auto. refl. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)