proposition: Lemma ExpP_P {τ} {e : Γ ⊢ τ} : ExpP e → P e.
proof: Proof. intros; induction τ; simpl in *; simp ExpP in X; now reduce. Qed.
imports: Category.Lib Category.Instance.Lambda.Ltac Category.Instance.Lambda.Ty Category.Instance.Lambda.Exp Category.Instance.Lambda.Sub Equations(Equations)