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