proposition: Corollary join_fmap_fmap_x `{MonadLaws m} : forall (a b : Type) (f : a -> b) x, join (fmap (fmap f) x) = fmap f (join x).
proof: Proof. intros. replace (fmap[m] f (join[m] x)) with ((fmap[m] f \o join[m]) x). rewrite <- join_fmap_fmap. reflexivity. reflexivity. Qed.
imports: Hask.Control.Applicative