Proper instance with `pointwise_relation` for `from_option`.

theories/option.v

@@ -21,7 +21,7 @@ Proof. congruence. Qed.
 (** The [from_option] is the eliminator for option. *)
 Definition from_option {A B} (f : A → B) (y : B) (mx : option A) : B :=
   match mx with None => y | Some x => f x end.
-Instance: Params (@from_option) 3 := {}.
+Instance: Params (@from_option) 2 := {}.
 Arguments from_option {_ _} _ _ !_ / : assert.
 
 (** The eliminator with the identity function. *)
@@ -145,8 +145,12 @@ Section setoids.
   Global Instance is_Some_proper : Proper ((≡@{option A}) ==> iff) is_Some.
   Proof. inversion_clear 1; split; eauto. Qed.
   Global Instance from_option_proper {B} (R : relation B) (f : A → B) :
-    Proper ((≡) ==> R) f → Proper (R ==> (≡) ==> R) (from_option f).
-  Proof. destruct 3; simpl; auto. Qed.
+    Proper ((≡) ==> R) f →
+    Proper (R ==> (≡) ==> R) (from_option f).
+  Proof. solve_proper. Qed.
+  Global Instance from_option_proper_ext {B} (R : relation B) :
+    Proper (pointwise_relation A R ==> R ==> (=) ==> R) from_option.
+  Proof. solve_proper. Qed.
 End setoids.
 
 Typeclasses Opaque option_equiv.