proposition: Lemma Value_irreducible {Γ τ} {e e' : Exp Γ τ} : ValueP e → ¬ (e ---> e').
proof: Proof. repeat intro. dependent induction H0; dependent elimination H; intuition eauto. Qed.
imports: Coq.Lists.List 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.Log Equations(Equations)