proposition: Lemma MoveB_Realise' m : MoveB m n ⊨ fun t '(l, t') => forall t_sig, t = [| encode_tape' t_sig |] -> t' = [| encode_tape' (mv m t_sig) |].
proof: Proof. eapply Realise_monotone. { eapply MoveB_Realise. } intros t (?, t') ? t_sig ->. rewrite (destruct_tape t') in *. specialize (H (mapTape f t_sig) eq_refl) as ->. f_equal. destruct t_sig, m; try reflexivity. - cbn. destruct l; cbn; reflexivity. - cbn. destruct l0; cbn; reflexivity. Qed.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi Undecidability.TM.Combinators.Combinators Undecidability.TM.Compound.WriteString