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