(*
 * Per the new thing described in the 24may02 implementation-notes entry, the
 * expression in the (first) axiom X = should NOT type check.
 *
 * 16jan06 update: OK, the first axiom X = does not type check, which is correct.
 * However, the ones commented with "should be an error" are wrong, I believe.
 * This MUST get ironed out.
 *)
object X;
object Y;
axiom A1 = forall (x:X) forall (y:Y) x = y;		-- ERROR

object Xa < X;
object Ya < Y;

axiom A2 = forall (xa:Xa) forall (ya:Ya) xa = ya;	-- should be an error

object X1 < X;
object X2 < X;
axiom A3 = forall (x1:X1) forall (x2:X2) x1 = x2;
axiom A4 = forall (x1:X1) forall (x2:X2) x1 = 1;	-- should be an error
axiom A5 = forall (x1:X1) forall (x2:X2) x1 = {1,2};	-- ERROR