<p>
For an equation of the form <code>X ≡<sub>A</sub> Y</code>,
where <code>X</code> and <code>Y</code> are types involved
in an assignment (including parameter passing and return statements),
the top-level type structures may unify loosely but element types
must unify exactly, matching the rules for assignments.
</p>

<p>
For an equation of the form <code>P ≡<sub>C</sub> C</code>,