> It is not. I am not sure about proof, but qed usually does a bit more
> than apply (e.g., solve things by assumption).
True, but shouldn't that mean that "by xy" solves more than "apply x apply
y done", instead of the other way round?