proposition: Lemma SubExp_ValueP {Γ Γ' τ} {v : Exp Γ τ} (σ : Sub Γ' Γ) : ValueP v → ValueP (SubExp σ v).
proof: Proof. intros X. now induction X; simpl; intros; try constructor. Defined.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Category.Instance.Lambda.Ren Equations(Equations)