proposition: Corollary join_fmap_join_x : ∀ a (x : (m ◯ m ◯ m) a), join (fmap join x) = join (join x).
proof: Proof. destruct m, M; simpl in *; intros. rewrite <- join_fmap_join; reflexivity. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Functor Category.Theory.Monad Category.Instance.Coq