obj Sex =  m:Male or f:Female;
obj Sex' =  'Male' or 'Female';	(* Should be same as Sex. *)

thm T1 = forall (s:Sex) s = 'Male'; (* Obviously false thm, but should type check*)
thm T2 = forall (s:Sex) s ?. m;

axiom A1 =
    forall (s:Sex)
	(s = 'Male') = s ?. m;	(* Type checking prob needs to be fixed. *)

(* Feb 09 Update: The two above-cited type checking problems have now in fact
 * been fixed.  Yipee. *)