src/ZF/equalities.thy
changeset 14610 9c2e31e483b2
parent 14171 0cab06e3bbd0
child 14883 ca000a495448