This is an advanced version of assignment A.
- Several students wanted to prove the property ‘if A has the form of X[Y]Z, then Y contains at least one propositional variable’. But this is insufficient to prove the exercise.
- If one wants to prove a property based on another property that one had proved to be true for all wffs, it would be better to combine these two properties and prove them together.
One of the interesting approaches is to prove that every wff does not contain either  or \sim ] or \vee ]. So suppose Y does not contain any propositional variables, we will find one of the three patterns above in X[Y]Z, which contradicts with the fact that X[Y]Z is well-formed.