proposition: Lemma Seq_Realise R1 R2 : pM1 ⊨ R1 -> pM2 ⊨ R2 -> Seq ⊨ ⋃_y ((R1 |_ y) ∘ R2).
proof: Proof. intros. eapply Realise_monotone. - eapply (Switch_Realise (R1 := R1) (R2 := (fun _ => R2))); eauto. - easy. Qed.
imports: Undecidability.TM(Util.TM_facts Switch)