proposition: Lemma decode_encode_space (x : space) : decode_space (encode_space x) = x.
proof: Proof. by apply: ListFin.decode_encode. Qed.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes PeanoNat Lia List ssreflect ssrbool ssrfun