proposition: Lemma image_add a A : image (add a A) [=] add (f a) (image A).
proof: Proof. intro x. split. fo. subst. fo. fo. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(LogicUtil RelUtil FunUtil ListUtil NatUtil ClassicUtil BoundNat)