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