proposition: Lemma RenVar_skip1 {τ τ' Γ} (v : Var Γ τ) : RenVar (skip1 (τ:=τ')) v = SV v.
proof: Proof. unfold skip1; simp RenVar. now rewrite RenVar_idRen. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Equations(Equations)