Proving a Replacement Theorem in Proposition Logic formulas. The Problem goes like this: 
"Assume $A$$1$ $\equiv$ $A$$2$ . Show that for any formula $C$-containing $A$$1$ as a part , if we replace one of more occurences of the part $A$$1$ by $A$$2$ , then the resulting formula is logically equivalent to $C$."
Attempt for a solution: Now, at first glance ,this theorem seems obvious to me , but I still have to prove it. My choice is to use the law of induction and the following identities (which can be derived from $A$$1$ $\equiv$ $A$$2$).
$1$.  $A$$1$ $\equiv$ $A$$2$ 
$2$.  ($\lnot$$A$$1$) $\equiv$ ($\lnot$$A$$2$)
$3$.  ($A$$1$) $d$ $B$ $\equiv$   ($A$$2$) $d$ $B$ 
$4$.  $B$ $d$ ($A$$1$)  $\equiv$ $B$ $d$ ($A$$1$) 
(Here $d\in\{\land,\lor,\Leftarrow,\Rightarrow,\Leftrightarrow\}$) 
But at this point I had no idea How to do the actual induction.Thankfully , A stackexchange user Answered this question like this:
"If $A_1$ is of degree $k$, then your base case is a formula containing $A_1$ as a part and of degree $k$. The only possible formula under those conditions is $A_1$ itself, so $A_1\equiv A_2$ is the base case, as you said.
Now suppose we have the result for all formulas containing $A_1$ as a part and of degree up to $n$ with $n\ge k$. Consider a formula $C$ containing $A_1$ as a part and of degree $n+1$. Since $C$ is of degree $n+1>n\ge k$ there is at least one propositional connective that doesn't belong to $A_1$.
Here is where you have to consider the cases where that extra propositional connective could be $\lnot$, $\lor$, $\land$, $\Rightarrow$, $\Leftarrow$, $\Leftrightarrow$; and separate $C$ is two different subformulas (one of them containing $A_1$ as a part, since we didn't break $A_1$). You apply your induction hypothesis in that subformula (we can because it is of degree $l$ with $k\le l\le n$, with the first inequality holding because it contains $A_1$) and replace $A_1$ for $A_2$ in that subformula.
Finally, justify that the whole formula, $C$, is equivalent to the one obtained replacing $A_1$ for $A_2$ knowing the equivalence of the subformula and using the propositional connective you're considering. Once you've considered all cases, you're done."
This was a nice solution with induction. And I thought I could make this solution a bit more Rigorous and formal for myself.So I started with it.
My Attempt: First of all , lets define a special kind of formula in this form,
$v$$m+1$(...($v_3$( $v_2(v_1   $($n$$1$$X$$1$ $d$$1$ $n$$2$$X$$2$$)$ $d$$2$ $n$$3$$X$$3$$)$ $d$$3$ $n$$4$$X$$4$$)...)$ $d$$m$$n$$m+1$$X$$m+1$$)$
Here ,
($1$) $X$ is a propositional formula .The sub numbers indicate that they can be different.
($2$) $d$ can be an "$or$" or an "$and$" or "$implies$" or "$Double$ $implies$".The sub numbers indicate that they can be different.
($3$) $n$ can be $negation$ or $nothing$.The sub numbers indicate that they can be different.
($4$) $v$ can be $negation$ or $nothing$.The sub numbers indicate that they can be different.
Example of this kind of formula is like this,
$(i)$ $((($ $\lnot$ ($A$ $\land$ $B$) $\lor$ $C$ $)$ $\land$ $D$ $)$ $\lor$ $\neg$$E$ $)$ 
$(ii)$ $(((($ $\neg$ ($A$ $\land$ $B$) $\rightarrow$ $C$ $)$ $\leftrightarrow$ $D$ $)$ $\lor$ $\neg$$E$ $)$ $\lor$ $B$ $)$
But formulas like below don't follow that form,
$(i)$ $($ $\lnot$ $($ $A$ $\land$ $B$) $\lor$ $($ $($ $C$ $\land$ $D$ $)$ $\lor$ $\neg$$E$ $)$ $)$ 
$(ii)$ $($ $\neg$ $($ $($ $A$ $\land$ $B$ $)$ $\rightarrow$ $C$ $)$ $\leftrightarrow$ $($ $($ $D$ $\lor$ $\neg$$E$ $)$ $\lor$ $B$ $)$ $)$ $)$
First , We will assume the formula $C$ in this question is in this form.Then,If $A_1$ is of degree $k$, then the base case is a formula $C$ containing $A_1$ as a part and of degree $k$. The only possible formula under those conditions is $A_1$ itself, so $A_1\equiv A_2$ is the base case.
Now suppose we have the result for all formulas containing $A_1$ as a part and of degree up to $n$ with $n\ge k$.Now, Lets say  $C_1^n$ is a formula with the following properties ,
$(i)$ It is of degree $n$. 
$(ii)$ It is in this form. 
$(iii)$ It has one or more instances of $A_1$. 
For the induction ,We assume that $C_1^n$ $\equiv$ $C_2^n$ Where $C_2^n$ is what we get after replacing all $A_1$ in $C_1^n$ by $A_2$.
To complete the induction , we have to prove that $C_1^{n+1}$ $\equiv$ $C_2^{n+1}$
Now , because $(n+1)$ is $1$ more than $n$ ,this means that means there is one extra logical connective in $C_1^{n+1}$ that doens't belong to $C_1^n$.This is where we have to consider all of the cases and prove that $C_1^{n+1}$ $\equiv$ $C_2^{n+1}$ using the fact that $C_1^n$ $\equiv$ $C_2^n$ and The equivalence identities shown at the very start.When we have proved for all of the cases that $C_1^{n+1}$ $\equiv$ $C_2^{n+1}$ , this will imply (By induction ) that $C_1$ $\equiv$ $C_2$ And we are done !
But here is a Problem , not all $C$ will be in this form (Like the examples I have shown).Then what will happen? I have tried like this :
Lets say there is a $C$ which is like this:
$(i)$ $($ $\lnot$ $($ $A_1$ $\land$ $B$ $)$ $\lor$ $($ $($ $A_1$ $\land$ $D$ $)$ $\lor$ $\neg$$E$ $)$ $)$ 
I Guess what I can do is that break the formula into two pieces like this,
$(i)$ $($ $A_1$ $\land$ $B$ $)$ 
$(ii)$ $($ $A_1$ $\land$ $D$ $)$ $\lor$ $\neg$$E$ $)$
And each of these "sub formulas" are in this form.So we can use the lemma that was proved earlier to prove equivalence for each cases (when replacing $A_1$ By $A_2$ ).and because each of these "sub formulas" have there equivalences preserved , the Entire formula C is equivalent (when replacing $A_1$ By $A_2$).
But now , lets say there is another formula C like this,
$($ $\lnot$ $($ $A_1$ $\land$ $B$ $)$ $\lor$ $($ $($ $A_1$ $\land$ $D$ $)$ $\lor$ $\neg$$E$ $)$ $)$ $\lor$ $($ $\lnot$ $($ $A_1$ $\land$ $B$ $)$ $\lor$ $($ $($ $A_1$ $\land$ $M$ $)$ $\lor$ $\neg$$E$ $)$ $)$
For this formula , we have to break the formula into $2$ different subformula ,and then break each of those two subformulas into $2$ more subformula .So we got a total of $4$ subformulas in this form.And now we have to prove the equivalence of each of those cases using the lemma to prove equivalence of the entire $C$.Now imagine that For any General C ,we had to break subformulas into subformulas into subformulas....At this point , I am stuck because I had no way of proving the equivalence of any general C Formally.Is there an algorithmic process that I have to apply at this point to prove this theorem formally $?$
 A: I agree that there is the problem with the proposed solution to your earlier question as you are indicating, in that the degree of the left operand of any binary connective can be different from the degree of its right operand.
I see two quick solutions here:

*

*Instead of using weak mathematical induction, use strong mathematical induction.  That is, show that a statement of degree $n$ has the property if you assume that all statements of degree smaller than $n$ have the property.


*Don't use induction over any numbers (whether those numbers reflect the 'degree' of a statement, or 'length' or ....) at all .. just use structural induction. That is, define your induction over the very recursive definition that defines the set of all propositional logic statements. So, you simply need to show that:
A. All atomic statements have the property
B. If $\phi_1$ and $\phi_2$ have the property, then:
i) $\neg \phi_1$ has the property
ii) $\phi_1 \land \phi_2$ has the property
... [you get the drift; just do it for all operators defined for your particular language]
Frankly. option 2) is by far the easiest one.
