proposition: Lemma eqdec_space : forall (x y : space), {x = y} + {x <> y}.
proof: Proof. have := @eqType_dec (TM.state M). move=> H. intros. do ? decide equality; by apply: H. Qed.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes PeanoNat Lia List ssreflect ssrbool ssrfun