proposition: Lemma TerminatesIn_monotone {n : nat} (M : TM n) (T T' : tRel sig n) : M ↓ T' -> (T <<=2 T') -> M ↓ T.
proof: Proof. intros H1 H2. firstorder. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM