proposition: Lemma renaming_update s y z : renaming s -> renaming (update y (Var z) s).
proof: Proof. intros [m hm]. exists (fun x => match eq_dec x y with left _ => z | _ => m x end). intro x. unfold Def.update. eq_dec x y. refl. apply hm. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)