proposition: Corollary join_fmap_pure_x `{MonadLaws m} : forall a x, join (fmap (pure (a:=a)) x) = x.
proof: Proof. intros. replace x with (id x) at 2; auto. rewrite <- join_fmap_pure. reflexivity. Qed.
imports: Hask.Control.Applicative