fact: Definition decide : Mpm2 * Config -> bool := fun '(M, c) => match decision M c with | inl _ => true | inr _ => false end.
imports: List ssrfun List PeanoNat Lia Operators_Properties ssreflect ssrbool ssrfun Undecidability.Synthetic.Definitions