About Equal.refl

[iacore]

If I understand the code correctly, in Kind2, Equal.refl is not a constructor, but a regular definition.

This may be problematic, where inductive constructors are injective, while normal definitions may not be