Consider the following sequence of forms.

Cab, CaCbc, ... CaCb...Cxy.

Suppose that we have some well-formed formula **W** which unifies with one of the above forms, which we'll call **X**. 

Meta-Thereom: If the last letter of **X** corresponds to a tautology in **W**, then **W** is a tautology.

Meta-Proof:  First, we'll consider the case when **X** is Cab.  By hypothesis, b is a tautology.  Thus, Cab=Ca1.  Ca1=1, so Cab is a tautology.

Consider the case where **W** unifies with CaCbc.  By hypothesis c is a tautology.  So, CaCbc=CaCb1.  Now since Cb1=1 also, CaCb1=Ca1.  Ca1 unifies with Cab.  By the previous case Cab is thus a tautology.  So, CaCbc is a tautology.  Consequently, **W** is a tautology.

Suppose that the result holds where **W** unifies with CaCb...Cxy.  We consider the successor form of  CaCb...CxCyz, which is now **X**.  By hypothesis z is a tautology, so CaCb...CxCyz= Ca...CxCy1.  Ca...CxCy1=Ca...Cx1, since Cy1=1.  Ca...Cx1 unifies with CaCb...Cxy.  CaCb...Cxy is a tautology by hypothesis, so, Ca...CxCy1 is a tautology.  Consequently, under the supposition, CaCb...CxCyz is a tautology.

Therefore, the meta-theorem holds.

Some examples:

CaCbCcCdCeCfCgChCiCjCpCqp is a tautology,
CaCbCcCdCeCfCgChCiCjCpp is a tautology

Further application: Let 1 qualify as a tautology.  If we try to evaluate a well-formed formula to see if it is a tautology not, we check the last place of the formula.  If we replace that letter with 1, and if it has a form in the above sequence of forms, it will qualify as a tautology.  Thus, if it is not a tautology, we replace the last letter with 0.  If that expression can or does evaluate to 0, then the original well-formed formula is not a tautology.  Otherwise, it does qualify as a tautology.