[simpl in *] breaks [admit] at end of theories/Grothendieck/ToCat.v