proposition: Lemma size_renaming1 : forall u s, renaming s -> size (subs1 s u) = size u.
proof: Proof. induction u; intros s hs; gen hs; intros [m hm]; simpl; auto. rewrite hm. refl. rewrite IHu. refl. exists (fun y => match eq_dec y x with left _ => x | _ => m y end). intro y. unfold Def.update. eq_dec y x. refl. apply hm. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)