Theorem exists_eq_subtype_mk_iff

Modification history