proposition: Lemma apply_pair_sndE A B C (f : B -> M C) (ab : A * B) D (g : A * C -> M D) : apply_pair_snd f ab >>= g = f ab.2 >>= (fun x => g (ab.1, x)).
proof: Proof. rewrite /apply_pair_snd bindA. by under eq_bind do rewrite bindretf. Qed.
imports: ssrmatching mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy