proposition: Lemma apply_triple_sndE A B C D (f : B -> M D) a b c E (g : A * D * C -> M E) : apply_triple_snd f (a, b, c) >>= g = f b >>= (fun x => g (a, x, c)).
proof: Proof. rewrite /apply_triple_snd /= bindA. by under eq_bind do rewrite bindretf. Qed.
imports: ssrmatching mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy