Buenas tardes.
Solamente quería confirmar que el uso de argumentos implícitos (usando {}) estaba permitido.
Para dar un ejemplo de la funcionalidad a la que me refiero, esta sería una forma de definir la función identidad explícitamente:
Definition exid (A: Set)(a: A): A := a.
Theorem exid_eq: forall (A: Set) (a: A), exid A a = a.
Proof.
intros.
reflexivity.
Qed.
Con argumentos implícitos se vería así:
Definition imid {A: Set}(a: A): A := a.
Theorem imid_eq: forall (A: Set) (a: A), imid a = a.
Proof.
intros.
reflexivity.
Qed.