Monadic bind for `option` is non-expansive.

Just one instnace.

added 1 commit

• b2106d27 - Monadic bind for `option` is non-expansive.

Compare with previous version

Could you also add the analogue of

Instance option_mjoin_proper `{Equiv A} :
  Proper ((≡) ==> (≡@{option (option A)})) mjoin.
Proof. destruct 1 as [?? []|]; simpl; by constructor. Qed.

Then we have fmap/mbind/mjoin, like we have for ≡.

added 1 commit

• b225ccb1 - Monadic bind & join for `option` are non-expansive.

Compare with previous version

Added.

resolved all discussions

mentioned in commit 7237ce0c

merged

Merged, thanks.