ᛒ
т.е. если бы сигнатура писалась как
Inductive eq (A : Type) (a: A) A : Prop
, то последний аргумент никак не определен и его надо указывать в конструкторе, а с переменной он будет фиксирован уже в любом случае (или также Inductive eq (A : Type) : (a : A) -> A -> Prop
)