proposition: Fact sbtm_op_length : length sbtm_op = 9.
proof: Proof. reflexivity. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils pos subcode sss) Undecidability.Synthetic(ReducibilityFacts) Undecidability.TM(SBTM pctm_defs)