proposition: Lemma RenVar_idRen {τ Γ} (v : Var Γ τ) : RenVar idRen v = v.
proof: Proof. induction v; simpl; simp RenVar; intros; auto. now rewrite IHv. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Equations(Equations)