Consider propositional logic.

Frege systems are textbook-style proof systems, with a finite set of logically sound axioms and rules. However you can generalise each axiom/rule with substitutions, replacing each variable simultaneously everywhere with a term. This is fine because if we take any propositional tautology and replace the variables, which can have value 0 or 1, with terms that can have value 0 or 1, the tautology is still guaranteed to evaluate to true under all assignments. Frege systems are all p-equivalent.

Frege systems normally only allow this for axioms and rules, but you can also soundly allow substitutions on derived formulas, as long as they are guaranteed to be tautological as well. This can be guaranteed by not allowing non-tautological assumptions anywhere in the proofs. The resulting system is known sometimes as Substitution Frege.

While Substitution Frege allows you to replace variables with terms. Extended Frege allows the opposite, to replace complicated formulas to be replaced with fresh variables (extension variables). This allows Extended Frege to avoid large complicated formulas. Extended Frege even allows extension variables that use previous extension variables in their definitions.

However extension and substitution don't seem very compatible to me. It would be wrong to substitute extension variables with terms that don't represent the formulas they actually represent and the assumptions now include non-tautological information: the definitions of extension variables.

A third variation is Circuit Frege, which is Frege but using circuits (which allow subformulae/subcircuits to be reused without rewriting them) instead of formulas.

Substitution Frege, Extended Frege and Circuit Frege are all p-equivalent. In other words, there is an efficient (polynomial time) algorithm that can take a proof in one format and transform it into a proof in the other. The proofs that these algorithms (p-simulations) exists, some of them seem obvious, others appear to involved non-trivial relationships between propositional proof complexity and theories of Bounded Arithmetic. Which I admit I don't fully understand yet.

Whether the tautology is a formula or a circuit should not fundamentally change the soundness of the substitution rule, you are just replacing the input variables (that can be 0 or 1) with terms (either formulas or circuits) than can be 0 or 1. So while extension and substitution seem incompatible circuitry and substitution do seem compatible. I'll call this system Circuit Frege with Substitutions.

The question I have is asking if you have a proof of a tautology f in Circuit Frege with Substitution, does there exist an efficient way to turn that into an Extended Frege proof of f (possibly using extension variables to represent the circuitry in f)? Does it make a difference if the substituted terms are formulas or circuits? Whom can I cite for these results?