proposition: Lemma size_rename1 x y u : size (rename1 x y u) = size u.
proof: Proof. unfold Def.rename1. rewrite size_renaming1. refl. apply renaming_single. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)