fact: Definition encode_config : config M -> TM_config := fun '(q, t) => TM_facts.mk_mconfig (Some q) (| encode_tape t |).
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes PeanoNat Lia List ssreflect ssrbool ssrfun