proposition: Lemma TerminatesIn_extend {n : nat} (M : TM n) (T : tRel sig n) : M ↓ T -> M ↓ (fun tin k => exists k', k' <= k /\ T tin k').
proof: Proof. intros HTerm. hnf in *. intros tin k. intros (k'&Hk'&HT). specialize HTerm with (1 := HT) as (oconf&HLoop). exists oconf. eapply loop_monotone; eauto. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM