proposition: Lemma apply_triple_snd_kleisli A B C D F (f : B -> M D) (g : D -> M F) (a : A) b (c : C) : apply_triple_snd (f >=> g) (a, b, c) = f b >>= (fun b' => apply_triple_snd g (a, b', c)).
proof: Proof. by rewrite /apply_triple_snd /= kleisliE bindA. Qed.
imports: ssrmatching mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy