Make it strong!

FEM/Algebra/AffineSpace_new.v

@@ -215,7 +215,8 @@ Context {E : AffineSpace V}.
 Lemma transl_EX :
   { f | forall (A : E), cancel (vect A) (f A) /\ cancel (f A) (vect A) }.
 Proof.
-assert (H : forall A : E, exists ! f, cancel (vect A) f /\ cancel f (vect A)).
+assert (H : forall A : E, { f | unique (fun g =>  cancel (vect A) g /\ cancel g (vect A)) f }).
+  intros A; destruct (vect_l_bij_EX )
   intros A; destruct (vect_l_bij A) as [f Hf1 Hf2]; exists f; split; [easy |].
   intros f' [Hf'1 Hf'2]; apply fun_ext; intros u.
   apply (vect_l_inj A); rewrite Hf2 Hf'2; easy.