Don't use the zonked-in-the-knot types to create a name for the axiom
in a closed type family.