proposition: Corollary mbc_law_1_x : forall b m `{MonadBaseControlLaws b m} a x, liftBaseWith (const (pure[b] x)) = @pure m _ a x.
proof: Proof. intros. rewrite <- (@mbc_law_1 b m _ _ _ _ _ _ _). reflexivity. Qed.
imports: Hask.Control.Monad Hask.Control.Monad.Base Hask.Control.Monad.Trans.State