(* 
 * Attempt to confirm that pairwise forall is equiv to nested forall.  What I'm
 * really after is a way to say this bogus logic:
 *
 *     forall (x,y in l) x != y
 *
 * which is intended to say that all elements of l are unique.  The problem is
 * that this can't work, since x and y must be equal at some point, since they
 * both range over all elements of l, and hence will be the same element at
 * some point.
 *
 * So, here's another attempt to say this:
 *
 *     forall (x in l)
 *       exists! (x in l) true
 *
 * but the deal here is, this looks kind of funky with the true body of
 * exists!.  Perhaps we'll end up defining exists! in terms of the indexed form
 * just below, which means we could use it as a short cut for that.  We'll see
 * on this.
 *
 * Let's try stating using indexed positions:
 *
 *     forall (i,j in [1..#l] | i != j)
 *       l[i] != l[j]
 *
 * Just for overall clarity, let's break this down to is supposed base form:
 *
 *     forall (i,j: integer |
 *                 i >= 1 and j >= 1 and i <= #l and j <= #l and i != j)
 *       l[i] != l[j]
 *
 * which is by the supposed equiv rules
 *
 *     forall (i,j: integer)
 *       if (i >= 1 and j >= 1 and i <= #l and j <= #l and i != j)
 *       then l[i] != l[j]
 *

 * So what happens to this when i = 0?  Well, by the
 * "no-fault-if-p-is-false-in-p-implies-q" rule, the elseless if is still true,
 * which is what we want.  I.e., with i = 0, the if ... then l[i] != l[j] is
 * unconditionally true, which is what we want.  There's further elaboration on
 * this idea in the 9dec04 entry of imple-ideas.me
 *
 * So, now, back to the discussion of what we're after here, viz., logic for
 * all elements of a list being unique.  It appears from the above that the
 * form that quantifiers over list positions works, whereas the one that uses
 * "x,y in l" won't work given that duplicate values can exist in any list.
 *
 * This is all pretty interesting, actually, and we should include it in the
 * ref manual in a discussion of common forms of quantification.  The immediate
 * bottom line here, once again, is that the quanifying via list index can
 * accomplish things that cannot be accomplished using the 'in' form of
 * quantification
 * 
 *)

obj L = T*;
obj T;
var l:L;

axiom A1 =
  forall (x,y in l)
    x != y;

axiom A2 =
  forall (x in l)
    forall (y in l)
      x != y;

axiom A3 =
  forall (x:T | x in l)
    forall (y:T | x in l)
      x != y;

axiom A4 =
  forall (x:T)
    x in l
      and
    forall (y:T)
      y in l
	and
      x != y;