proposition: Corollary values_final {Γ τ} {e e' : Exp Γ τ} : e --->* e' → ValueP e → e = e'.
proof: Proof. intros. apply value_is_nf in H. unfold normal_form in H. induction X; auto. now intuition. 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.Sem Category.Instance.Lambda.Step Equations(Equations)