proposition: Corollary NoSub_idSub : NoSub (Γ:=[]) = idSub.
proof: Proof. reflexivity. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Category.Instance.Lambda.Ren Equations(Equations)