Quote:

Subformula property is neat, and it allows proving that something is not derivable without invoking models.

Do you say this restricted to the constructive context? I would think classically we can prove something is not derivable without invoking models, no?

There is an analog of subformula property for classical logic as well, but I don't remember the details. See "Basic proof theory" by Troelstra and Schwichtenberg. Quote:

For example, if p \/ ~p were provable in constructive logic for a propositional variable p, then it had to be derived either from p or ~p, which in turn could only be derived from p, a contradiction.

If I understand this correctly, it is because the only subformulas of p v ¬p are p and ¬p, and their subformulas only consist of p, each. Where exactly is the contradiction? That we cannot derive ¬p from p alone?

We can't derive p with no open assumptions because p is a propositional variable (and thus not a tautology). Actually, Jeremy Avigad has a more thorough proof in the article you found.