 Subformula replacement theorem

Replacing one designated subformula occurrence in a propositional formula by another propositional formula preserves well-formedness. Induct on the context surrounding the occurrence: at the root the result is the replacement formula; under a connective apply the induction hypothesis to the affected child and rebuild the parent using its formation rule.