proposition: Lemma SubExp_idSub {Γ τ} (e : Exp Γ τ) : SubExp idSub e = e.
proof: Proof. induction e; simpl; auto; rewrite ?IHe, ?IHe1, ?IHe2, ?IHe3; auto. - now rewrite SubVar_idSub. - f_equal. rewrite <- IHe at 2. now f_equal. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Category.Instance.Lambda.Ren Equations(Equations)