Extending the Static Checker(How to extend Rodin Tutorial)