proposition: Lemma rename_var y z x : rename y z (Var x) = Var (if eqb x y then z else x).
proof: Proof. unfold Def.rename, Def.single, Def.update, eqb; simpl. eq_dec x y; refl. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)