proposition: Lemma ReadB_Realise' : ReadB n ⊨ fun t '(l, t') => forall t_sig : tape Σ, t = [| encode_tape' t_sig |] -> t' = t /\ l = map_opt f (current t_sig).
proof: Proof. eapply Realise_monotone. { eapply ReadB_Realise. } intros t (?, t') ? t_sig ->. rewrite (destruct_tape t') in *. specialize (H (mapTape f t_sig) eq_refl) as [-> ->]. split; [reflexivity|]. eapply mapTape_current. Qed.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi Undecidability.TM.Combinators.Combinators Undecidability.TM.Compound.WriteString