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.
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?
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.
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?