src/ZF/equalities.thy
changeset 14343 6bc647f472b9
parent 14171 0cab06e3bbd0
child 14883 ca000a495448