proposition: Lemma step_preserves_SN' {Γ τ} {e e' : Γ ⊢ τ} : (e ---> e') → SN e' → SN e.
proof: Proof. intros. induction τ; simpl in *; pose proof H as H2; apply step_preserves_halting in H2; firstorder. 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)