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