 Propositional variable elimination

The displayed identity follows by testing the two possible truth values of $p$. Existentially forgetting $p$ gives $A[p:=\top ]\vee A[p:=\perp ]$. Repeating this operation produces a propositional formula on a specified remaining vocabulary. Logical truth constants are needed if that vocabulary is empty.