proposition: Lemma step_preserves_halting {Γ τ} (e e' : Exp Γ τ) : (e ---> e') → (halts e ↔ halts e').
proof: Proof. intros. unfold halts. split. - intros [e'' [H1 H2]]. + destruct H1. * apply value_is_nf in H2. now edestruct H2; eauto. * rewrite (Step_deterministic _ _ _ _ _ H s). now intuition eauto. - intros [e'0 [H1 H2]]. + exists e'0. split; auto. now eapply multi_step; eauto. Qed.
imports: Category.Lib Category.Instance.Lambda.Ltac Category.Instance.Lambda.Ty Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Category.Instance.Lambda.Ren Category.Instance.Lambda.Sub Category.Instance.Lambda.Log Category.Instance.Lambda.Sem Category.Instance.Lambda.Multi Category.Instance.Lambda.Sound Category.Instance.Lambda.Step Equations(Equations)