proposition: Lemma in_image_prove_eq : forall A B x (f : A -> B) (E : set A), x \in E -> f x \in image f E.
proof: Proof. Proof using. introv N. unfold image. rew_set. exists* x. Qed.
imports: TLC(LibTactics LibLogic LibContainer LibSet)