proposition: Theorem monad_law_4_x : forall (M : Type -> Type) (m_dict : Monad M) A B (f : A -> B) (x : M (M A)), join (fmap (fmap f) x) = fmap f (join x).
proof: Proof. intros. assert (join (fmap (fmap f) x) = (join ∘ fmap (fmap f)) x). unfold compose. reflexivity. assert (fmap f (join x) = (fmap f ∘ join) x). unfold compose. reflexivity. rewrite H. rewrite H0. rewrite monad_law_4. reflexivity. Qed.
imports: Applicative Coq.Lists.List