Consider that formulas in propositional logical can be represented as sets of bit-vectors. For example, a formula $\neg b$ (all bit-vectors of the type $?0?$) with three atomic propositions $a,b$ and $c$ represents the set
$$\{ 000, 101, 001, 100 \}.$$
Now given two sets given by formulas $(a \to b) \lor c$ (lets call this $f$) and $a \lor (\neg c \to b)$ (and this $g$), find a formula that tests whether the sets produced by these formulas are equal, $g$ is a subset of the $f$ and if $g$ is a proper subset of $f$.
My idea is that the equality could be tested as follows. If the set produced by the formula
$$\neg (f \Leftrightarrow g)$$
is empty, then the sets are equal. My idea is that for all evaluations of $a,b$ and $c$ the equivalence should produce true value and therefore the negation should produce empty set if $f = g$. For the proper subset test, I think a similar idea could be used:
$$\neg (g \to f).$$
Which should state in my mind that all the elements of $g$ must be in $f$ (for evaluation in which $f$ is true, the implications is also true), but $f$ can have other elements as well. So if it is again a empty set, then $g \subseteq f$. I'm not sure how to device the proper subset thought. Does my tests make sense and is the proper subset a trivial test as well?