LOGICAL INCONSISTENCY closed
LOGICAL INCONSISTENCY closed

def c bool (forall ' lam A x \ ! y \ x = y)

allowed from c = c to prove the absurd instantiating A twice with the
unit and boolean type.

The standard fix in HOL consists in:
1. every constant carry around its type
2. every type variable in the body must occur in the type

Instead we have followed System-F style:
1. when a constant is polymorphic it MUST be fully applied to type
   instances (via ''). E.g.  c '' bool
2. reflexivity fails when the type arguments are not the same:
   c '' bool = c '' (bool --> bool) is unprovable, preventing the
   paradox

NOTES:
1. the syntax for theorem and definition declarations is now uglier
2. new_basic_types are back to being only monomorphic

LPCIC/elpi