proposition: Lemma Seq_RealiseIn (R1 : Rel _ _) (R2 : Rel _ (F2 * _)) k1 k2: pM1 ⊨c(k1) R1 -> pM2 ⊨c(k2) R2 -> Seq ⊨c(1 + k1 + k2) ⋃_y ((R1 |_y) ∘ R2).
proof: Proof. intros H1 H2. eapply RealiseIn_monotone. - eapply (Switch_RealiseIn). + eapply H1. + intros f. eapply H2. - lia. - easy. Qed.
imports: Undecidability.TM(Util.TM_facts Switch)