proposition: Lemma SubVar_idSub {Γ τ} (v : Var Γ τ) : SubVar idSub v = VAR v.
proof: Proof. induction v; simpl; simp SubVar; auto. rewrite SubVar_ScR. rewrite IHv. simpl. now rewrite RenVar_skip1. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Category.Instance.Lambda.Ren Equations(Equations)