proposition: Lemma ValueP_dec {Γ τ} (e : Exp Γ τ) : ValueP Γ e ∨ ¬ ValueP Γ e.
proof: Proof. induction e; try solve [now left|now right]. destruct IHe1, IHe2. - left. now constructor. - right. intro. dependent elimination H. contradiction. - right. intro. dependent elimination H. contradiction. - right. intro. dependent elimination H. contradiction. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Exp Equations(Equations)