proposition: Lemma in_image_prove : forall A B x y (f : A -> B) (E : set A), x \in E -> y = f x -> y \in image f E.
proof: Proof. Proof using. intros. subst. applys* in_image_prove_eq. Qed.
imports: TLC(LibTactics LibLogic LibContainer LibSet)