proposition: Lemma basic_instructions : forall op, In op M -> basic op.
proof: Proof. Proof using basic_M. by apply /Forall_forall. Qed.
imports: List Lia Relation_Operators Operators_Properties Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(Nat_facts List_facts SMN_facts) Undecidability.StackMachines.Util.SMN_transform ssreflect ssrbool ssrfun