Every mathematical theorem is a tautologyI would like to be able to have a proof A that there is a proof B about something non-tautological.

The thing hat comes to mind is the Henkin's proof of completeness. One can formalize the semantics of, say, propositional logic, in Peano arithmetic and prove completeness by showing that if a formula is not derivable, then there exists a countermodel. Under the assumption that the formula is a tautology, this will yield a nonconstructive proof that the formula is derivable. It is probably possible to do this not only for propositional logic, but for some fragments of first-order logic, such as for formulas with at most n nested alternating quantifiers.

Note, by the way, that any proof of Prov_T("S") is notessentiallynonconstructive because there is an algorithm (Gödel–Gentzen negative translation) that turns any such proof into a constructive one. Please ask if you need more details about this.