soft question - Can you prove equivalence without being able to calculate it?

I give you this example, from the upper edge of the propositional calculus hierarchy:

cardinal equivalence:
For each boolean formula, |quantifications| = |assignments|.

Abstractly, the linear induction on n variables is provable using all the basics: True, Nil, union, intersection, +, =, zero, and +1, upon the number of variables. Set cardinality is the principle primitive operation, used in every part of the proof.
The key final lines look roughly like:
|Qa union Qb| + |Qa intersets Qb| = |Qa| + |Qb|.
and so then, |Q| = |Qa| + |Qb| = |Pa| + |Pb| = |P|.

The base case on zero variables has two parts, the True case, and the Nil case. The induction proceeds by substituting (True, Nil) for the first variable, obtaining two smaller formulas, called Pa, and Pb. The hypothesis |Q| = |P| applies to the two smaller formulas.

Okay, so. The equivalence is clearly a fundamental identity.
However.

However, one to one mapping between satisfying assignments and valid quantifications is generally out of the question, as far as I know (else PSpace = NP would nearly follow). quantifications refer to subsets, subsets of subsets, ..., with arbitrary alternations admitting deeply rich subset structures, of the original set of satisfying assignments. So, quantifications are "encodable" by something the same size as an assignment,
but the one to one map you are asking for is Unknown, in general.
I suppose thats different from saying "it does not exist".

And it does exist for the special case, for monotone boolean formulas. The map between assignments and valid quantifications is straightforward, and is the most obvious linear map any amateur could attempt to construct between valid quantifications and satisfying assignments. I suggest that the 2cnf to 2qbf p to Q solution map could be more studied, for details on how to construct such, or else why such would fail in general. I have not gotten around to that yet.

In general, counting assignments is in a class by itself, called #P. An amateur may presume a class called #Q, too; a professional would give details.

+++

By the way, I am still asking: is this identity known by any other name?
I tried calling it #P=#Q, twelve years ago, few knew what #P was,
and #Q was too deep to describe in emails, way back then.