proposition: Lemma RenExp_idRen {τ Γ} (e : Exp Γ τ) : RenExp idRen e = e.
proof: Proof. induction e; simpl; simp RenVar; simpl; intros; auto; rewrite ?IHe, ?IHe1, ?IHe2, ?IHe3; auto. - now rewrite RenVar_idRen. - now rewrite Keep_idRen, IHe. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Equations(Equations)