Slightly simpler version of Leibniz equality from the ML 2010 talk
  http://okmij.org/ftp/ML/first-class-modules/0README.dr

The differences are:

  * Only the eq type, the refl function and the Subst module are
    primitive; cast is now implemented in terms of Subst.

  * The Subst module now has a different type and a much shorter
    implementation.  The previous type of subst was:

       module Subst (TC : TyCon) :
       sig
         val subst : ('a, 'b) eq -> ('a TC.tc 'b TC.tc) eq
       end

    The new type of subst is:

       module Subst (TC : TyCon) :
       sig
         val subst : ('a, 'b) eq -> 'a TC.tc -> 'b TC.tc
       end

    The old Subst module is definable in terms of the new, because

       (a TC.tc, - TC.tc) eq

    is a type context.  The file contains an implementation, called
    Lift.

  * The type of refl has been changed from

       val refl : unit -> ('a, 'a) eq

    to

       val refl : ('a, 'a) eq

  * The locally-abstract type syntax is used to shorten some
    definitions.  We write

       let symm : type a b. (a, b) eq -> (b, a) eq =
         fun a_eq_b -> ...

    instead of

       let symm : 'a 'b. ('a, 'b) eq -> ('b, 'a) eq =
         fun (type a) (type b) a_eq_b -> ...