proposition: Lemma surj_set_image_surjective : surjective surj_set_image.
proof: Proof. red in |- *. simpl in |- *. unfold subtype_image_equal in |- *. simpl in |- *. unfold image_map in |- *. intros y; try assumption. elim y. intros x' subtype_prf; try assumption. elim subtype_prf. intros x H'; try assumption. exists x; try assumption. elim H'; intros H'0 H'1; try exact H'1; clear H'. Qed.
imports: Classical_Prop Parts