proposition: Theorem Exp_SN {τ} (e : Exp nil τ) : SN e.
proof: Proof. intros. replace e with (SubExp (Γ:=nil) NoSub e). - apply SubExp_SN. now constructor. - now rewrite NoSub_idSub, SubExp_idSub. 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)