proposition: Corollary SubExp_closed `(s : Sub [] []) `(e : [] ⊢ τ) : SubExp s e = e.
proof: Proof. dependent elimination s; simpl. rewrite NoSub_idSub. now rewrite SubExp_idSub. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Category.Instance.Lambda.Ren Equations(Equations)