proposition: Lemma RenExp_preserves_size {Γ Γ' τ} (r : Ren Γ Γ') (e : Exp Γ' τ) : Exp_size (RenExp r e) = Exp_size e.
proof: Proof. generalize dependent r. generalize dependent Γ. now induction e; simpl; simp RcR; simpl; intros; auto. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Equations(Equations)