INDUCTIVE DEFINITION eq () [ A:Set, :A ]
OF ARITY A→Prop
BUILT FROM:
     refl_equal: eq A x x