Proof without image_eq.

Lebesgue/Subset.v

@@ -144,6 +144,7 @@ Variable A1 : U1 -> Prop. (* Subset. *)
 Variable A2 : U2 -> Prop. (* Subset. *)
 
 Inductive image : U2 -> Prop := Im : forall x1, A1 x1 -> image (f x1).
+
 Definition image_ex : U2 -> Prop :=
   fun x2 => exists x1, A1 x1 /\ x2 = f x1.
 
@@ -1936,8 +1937,7 @@ Lemma preimage_empty_equiv :
   forall A2, empty (preimage f A2) <-> disj A2 (image f fullset).
 Proof.
 intros A2; split.
-rewrite image_eq.
-intros HA2 x2 Hx2 [x1 [_ Hx1]]; apply (HA2 x1); rewrite Hx1 in Hx2; easy.
+intros HA2 x2 Hx2a Hx2b; induction Hx2b as [x1 Hx1]; apply (HA2 x1); easy.
 intros HA2 x1 Hx1; apply (HA2 (f x1)); easy.
 Qed.