proposition: Lemma in_image : forall (A : part_set E) (x : E) (y : F), in_part x A -> Equal y (f x) -> in_part y (image A).
proof: Proof. simpl in |- *; auto with algebra. intros A x y H' H'0; try assumption. exists x; split; [ try assumption | idtac ]; auto with algebra. Qed.
imports: Classical_Prop Parts