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