proposition: Lemma If_Realise R1 R2 R3 : pM1 ⊨ R1 -> pM2 ⊨ R2 -> pM3 ⊨ R3 -> If ⊨ (R1 |_true) ∘ R2 ∪ (R1 |_false) ∘ R3.
proof: Proof. intros. eapply Realise_monotone. - eapply (Switch_Realise (R1 := R1) (R2 := (fun b => if b then R2 else R3))); eauto. now intros []. - hnf. intros H2 (f& t). intros ([ | ]& (y & H3&H3')). + left. hnf. eauto. + right. hnf. eauto. Qed.
imports: Undecidability.TM(Util.TM_facts Switch)