- Fix getSomeOperateSing remvoe (SingKind ts) Constraint
- 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.
- Fix getSomeOperateSing
- Improve runOperate