Module Type A. Axiom f : True. End A.
Module M8416 : A. Definition f := I. End M8416.