proposition: Lemma Realise_strengthen n (F : Type) (pM : pTM F n) R1 R2 : Realise pM R2 -> Realise pM R1 -> Realise pM (R1 ∩ R2).
proof: Proof. intros HwR HR t. firstorder. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM