proposition: Corollary Exp_size_preserved {Γ τ} (e1 e2 : Exp Γ τ) : Exp_size e1 ≠ Exp_size e2 → e1 ≠ e2.
proof: Proof. repeat intro; subst; contradiction. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Ty Equations(Equations)