proposition: Lemma WriteB_Realise' (c : option Σ) : WriteB (map_opt f c) ⊨ fun t '(_, t') => forall t_sig, t = [| encode_tape' t_sig |] -> t' = [| encode_tape' (wr c t_sig) |].
proof: Proof. eapply Realise_monotone. { eapply WriteB_Realise. } intros t (?, t') ? t_sig ->. rewrite (destruct_tape t') in *. specialize (H (mapTape f t_sig) eq_refl) as ->. unfold tape_write. destruct c. - cbn. destruct t_sig; reflexivity. - reflexivity. Qed.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi Undecidability.TM.Combinators.Combinators Undecidability.TM.Compound.WriteString