proposition: Lemma construct_trans_spec {n : nat} (f : (Fin.t n) * bool -> option ((Fin.t n) * bool * direction)) : forall x, trans' (Build_SBTM n (construct_trans f)) x = f x.
proof: Proof. move=> /= [q a]. rewrite /trans' /construct_trans /=. rewrite (Vector.nth_map _ _ q q erefl) seq_Vector_spec. by case: a. Qed.
imports: Undecidability(TM.SBTM) PeanoNat Lia List ssreflect ssrbool ssrfun