proposition: Lemma image_singleton x : image (singleton x) [=] singleton (f x).
proof: Proof. unfold singleton. rewrite image_add, image_empty. refl. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(LogicUtil RelUtil FunUtil ListUtil NatUtil ClassicUtil BoundNat)