proposition: Lemma in_image_inv : forall A B y (f : A -> B) (E : set A), y \in image f E -> exists x, x \in E /\ y = f x.
proof: Proof. Proof using. introv N. unfolds image. rew_set in N. auto. Qed.
imports: TLC(LibTactics LibLogic LibContainer LibSet)