proposition: Lemma RenExp_DropAll {τ} (e : Exp [] τ) : RenExp DropAll e = e.
proof: Proof. rewrite DropAll_nil_idRen. now rewrite RenExp_idRen. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Equations(Equations)