Missing instantiation of inner/nested quantifier

[mschwerhoff]

Note: Reducing attached SMT file to its minimum revealed issue #26.

Running SMT file set_equals_triggers_datatypes.smt2.txt on Z3 4.8.6 on Windows 10 produced
z3.log. Loading this into the axiom profiler shows an instantiation of axiom Set_equal_outer, and instantiations of datatype axioms that are triggered by terms that — I believe — have been obtained from instantiating axiom Set_equal_inner. According to the profiler, however, the latter was not instantiated.