proposition: Lemma While_TerminatesIn : pM ⊨ R -> projT1 pM ↓ T -> WhileTM ↓ While_T.
proof: Proof. intros HRel HTerm. eapply While_TerminatesIn_ind; eauto. intros tin k' HCoInd. destruct HCoInd as [ t k k1 H1 H2 H3 ]. eauto. Qed.
imports: Undecidability(TM.Util.TM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts