proposition: Lemma SubExp_VAR_ZV {Γ τ} (s : Sub [] Γ) (x : Exp [] τ) : SubExp (Push x s) (VAR ZV) = x.
proof: Proof. now simpl; simp SubVar. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Category.Instance.Lambda.Ren Equations(Equations)