proposition: Lemma size_replace_all : forall x y t, size (replace_all x y t) = size t.
proof: Proof. intros x y. induction t; simpl. refl. refl. rewrite IHt1, IHt2. refl. rewrite IHt. refl. Qed.
imports: CoLoR(LogicUtil LAlpha RelUtil BoolUtil) Coq(Morphisms)