fact: Definition normal_form_of {Γ τ} (e e' : Exp Γ τ) : Type := (e --->* e' ∧ normal_form Step e').
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)