diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,11 @@
 # Revision history for typed-fsm
 
+## 0.3.0.0-- 2024-7-25
+* Remove the SingI constraints from SomeMsg and AnyMsg.
+* Modify the definition of LiftM and remove the SingI constraints.
+* RunOperate and runOp both remove the SingI constraints.
+* Reason for doing this: When explaining Ast, constraints can be easily converted into proofs, but proofs seem difficult to convert into constraints.
+
 ## 0.2.0.1-- 2024-7-22
 
 * Fix getSomeOperateSing
diff --git a/src/TypedFsm/Core.hs b/src/TypedFsm/Core.hs
--- a/src/TypedFsm/Core.hs
+++ b/src/TypedFsm/Core.hs
@@ -12,7 +12,7 @@
  )
 
 import Data.Kind (Type)
-import Data.Singletons (SingI)
+import Data.Singletons (Sing, SingI (..))
 
 -- | The state-transition type class
 class StateTransMsg ps where
@@ -33,8 +33,8 @@
 data Operate :: (Type -> Type) -> (ps -> Type) -> ps -> Type where
   IReturn :: ia (mode :: ps) -> Operate m ia mode
   LiftM
-    :: (SingI mode, SingI mode')
-    => m (Operate m ia mode')
+    :: Sing mode'
+    -> m (Operate m ia mode')
     -> Operate m ia mode
   In
     :: forall ps m (from :: ps) ia
@@ -44,13 +44,13 @@
 instance (Functor m) => IFunctor (Operate m) where
   imap f = \case
     IReturn ia -> IReturn (f ia)
-    LiftM f' -> LiftM (fmap (imap f) f')
+    LiftM s f' -> LiftM s (fmap (imap f) f')
     In cont -> In (imap f . cont)
 instance (Functor m) => IMonad (Operate m) where
   ireturn = IReturn
   ibind f = \case
     IReturn ia -> (f ia)
-    LiftM m -> LiftM (fmap (ibind f) m)
+    LiftM s m -> LiftM s (fmap (ibind f) m)
     In cont -> In (ibind f . cont)
 
 -- | get messages from outside
@@ -59,4 +59,4 @@
 
 -- | lifts the internal `m a` to `Operate m (At a i) i'
 liftm :: forall ps m (mode :: ps) a. (Functor m, SingI mode) => m a -> Operate m (At a mode) mode
-liftm m = LiftM (returnAt <$> m)
+liftm m = LiftM sing (returnAt <$> m)
diff --git a/src/TypedFsm/Driver/Common.hs b/src/TypedFsm/Driver/Common.hs
--- a/src/TypedFsm/Driver/Common.hs
+++ b/src/TypedFsm/Driver/Common.hs
@@ -7,31 +7,28 @@
 module TypedFsm.Driver.Common where
 
 import Data.IFunctor (At (..))
-import Data.Singletons (Sing, SingI (..), SingKind (..))
+import Data.Singletons (Sing, SingKind (..))
 import TypedFsm.Core (Operate (..), StateTransMsg (Msg))
 import Unsafe.Coerce (unsafeCoerce)
 
 data SomeOperate ts m a
   = forall (i :: ts) (o :: ts).
-    (SingI i) =>
-    SomeOperate (Operate m (At a o) i)
+    SomeOperate (Sing i) (Operate m (At a o) i)
 
 getSomeOperateSing :: (SingKind ts) => SomeOperate ts m a -> Sing (r :: ts)
-getSomeOperateSing (SomeOperate (_ :: Operate m ia i)) =
-  unsafeCoerce $ sing @i
+getSomeOperateSing (SomeOperate si (_ :: Operate m ia i)) =
+  unsafeCoerce si
 
 getSomeOperateSt :: (SingKind ts) => SomeOperate ts m a -> Demote ts
-getSomeOperateSt (SomeOperate (_ :: Operate m ia i)) = fromSing $ sing @i
+getSomeOperateSt (SomeOperate si (_ :: Operate m ia i)) = fromSing $ si
 
 data SomeMsg ps from
   = forall (to :: ps).
-    (SingI to) =>
-    SomeMsg (Msg ps from to)
+    SomeMsg (Sing to) (Msg ps from to)
 
 data AnyMsg ps
   = forall (from :: ps) (to :: ps).
-    (SingI from, SingI to) =>
-    AnyMsg (Msg ps from to)
+    AnyMsg (Sing from) (Sing to) (Msg ps from to)
 
 {- | Reuslt of run FSM
 
diff --git a/src/TypedFsm/Driver/General.hs b/src/TypedFsm/Driver/General.hs
--- a/src/TypedFsm/Driver/General.hs
+++ b/src/TypedFsm/Driver/General.hs
@@ -10,20 +10,20 @@
 import Data.Bool.Singletons (SBool (..))
 import Data.Eq.Singletons (SEq (..))
 import Data.IFunctor (At (..))
-import Data.Singletons (SingI (..))
+import Data.Singletons (Sing)
 import TypedFsm.Core (Operate (..), StateTransMsg (Msg))
 import TypedFsm.Driver.Common
 import Unsafe.Coerce (unsafeCoerce)
 
 anyToSomeMsg
   :: forall ps input
-   . (SingI input, SEq ps)
-  => AnyMsg ps -> Maybe (SomeMsg ps input)
-anyToSomeMsg (AnyMsg (msg :: Msg ps from to)) =
-  case sing @from %== sing @input of
+   . (SEq ps)
+  => Sing input -> AnyMsg ps -> Maybe (SomeMsg ps input)
+anyToSomeMsg sinput (AnyMsg sfrom sto (msg :: Msg ps from to)) =
+  case sfrom %== sinput of
     -- (from == input) ~ True
     -- ==> from ~ input
-    STrue -> unsafeCoerce (Just (SomeMsg msg))
+    STrue -> unsafeCoerce (Just (SomeMsg sto msg))
     SFalse -> Nothing
 
 newtype UnexpectMsg ps = UnexpectMsg (AnyMsg ps)
@@ -36,23 +36,23 @@
 runOperate
   :: forall ps m a (input :: ps) (output :: ps)
    . ( Monad m
-     , SingI input
      , SEq ps
      )
   => UnexpectMsgHandler ps m
   -> [AnyMsg ps]
+  -> Sing input
   -> Operate m (At a output) input
   -> m (Result ps (UnexpectMsg ps) m a)
-runOperate unHandler anyMsgs = \case
+runOperate unHandler anyMsgs sinput = \case
   IReturn (At a) -> pure (Finish a)
-  LiftM m -> m >>= (runOperate unHandler anyMsgs)
+  LiftM singv m -> m >>= (runOperate unHandler anyMsgs singv)
   In f -> loop anyMsgs
    where
-    loop [] = pure $ Cont $ SomeOperate (In f)
+    loop [] = pure $ Cont $ SomeOperate sinput (In f)
     loop (anyMsg : evns') = do
-      case anyToSomeMsg @_ @input anyMsg of
+      case anyToSomeMsg sinput anyMsg of
         Nothing -> case unHandler of
           Ignore -> loop evns'
           IgnoreAndTrace trace -> trace anyMsg >> loop evns'
           Terminal -> pure (ErrorInfo $ UnexpectMsg anyMsg)
-        Just (SomeMsg msg) -> runOperate unHandler evns' (f msg)
+        Just (SomeMsg sto msg) -> runOperate unHandler evns' sto (f msg)
diff --git a/src/TypedFsm/Driver/Op.hs b/src/TypedFsm/Driver/Op.hs
--- a/src/TypedFsm/Driver/Op.hs
+++ b/src/TypedFsm/Driver/Op.hs
@@ -16,7 +16,7 @@
 import Data.GADT.Compare (GCompare, GOrdering (..))
 import Data.IFunctor (At (..))
 import Data.Ord.Singletons (SOrd (sCompare), SOrdering (..))
-import Data.Singletons (Sing, SingI (..), SomeSing (..))
+import Data.Singletons (Sing, SomeSing (..))
 import TypedFsm.Core (Operate (..))
 import TypedFsm.Driver.Common
 import Unsafe.Coerce (unsafeCoerce)
@@ -58,26 +58,24 @@
 
 runOp
   :: forall ps event state m a (input :: ps) (output :: ps)
-   . ( SingI input
-     , GCompare (Sing @ps)
-     )
+   . (GCompare (Sing @ps))
   => (Monad m)
   => State2GenMsg ps state event
   -> [event]
+  -> Sing input
   -> Operate (StateT state m) (At a output) input
   -> (StateT state m) (Result ps (NotFoundGenMsg ps) (StateT state m) a)
-runOp dmp evns = \case
+runOp dmp evns sinput = \case
   IReturn (At a) -> pure (Finish a)
-  LiftM m -> m >>= runOp dmp evns
+  LiftM sinput' m -> m >>= runOp dmp evns sinput'
   In f -> do
-    let singInput = sing @input
-    case D.lookup singInput dmp of
-      Nothing -> pure (ErrorInfo $ NotFoundGenMsg $ SomeSing singInput)
+    case D.lookup sinput dmp of
+      Nothing -> pure (ErrorInfo $ NotFoundGenMsg $ SomeSing sinput)
       Just (GenMsg genMsg) -> loop evns
        where
-        loop [] = pure $ Cont $ SomeOperate (In f)
+        loop [] = pure $ Cont $ SomeOperate sinput (In f)
         loop (et : evns') = do
           state' <- get
           case genMsg state' et of
             Nothing -> loop evns'
-            Just (SomeMsg msg) -> runOp dmp evns' (f msg)
+            Just (SomeMsg sto msg) -> runOp dmp evns' sto (f msg)
diff --git a/typed-fsm.cabal b/typed-fsm.cabal
--- a/typed-fsm.cabal
+++ b/typed-fsm.cabal
@@ -20,7 +20,7 @@
 -- PVP summary:     +-+------- breaking API changes
 --                  | | +----- non-breaking API additions
 --                  | | | +--- code changes with no API change
-version:            0.2.0.1
+version:            0.3.0.0
 
 -- A short (one-line) description of the package.
 synopsis: A framework for strongly typed FSM