proposition: Corollary join_fmap_ret_x : ∀ a x, join (fmap (ret (x:=a)) x) = x.
proof: Proof. intros. replace x with (id x) at 2; auto. pose proof (@join_fmap_ret Coq m M a) as HA. rewrites; reflexivity. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Functor Category.Theory.Monad Category.Instance.Coq