-ndefinition function_space_setoid: setoid → setoid → setoid.
- #A; #B; napply (mk_setoid …);
-##[ napply (function_space A B);
-##| #f; #f1; napply (∀a:A. proofs (eq … (f a) (f1 a)));
-##| nwhd; #x; #a;
- napply (f_ok … x …); (* QUI!! *)
-(* unfold carr; unfold proofs; simplify;
- apply (refl A)
- | simplify;
- intros;
- unfold carr; unfold proofs; simplify;
- apply (sym B);
- apply (f a)
- | simplify;
- intros;
- unfold carr; unfold proofs; simplify;
- apply (trans B ? (y a));
- [ apply (f a)
- | apply (f1 a)]]
-qed.
+interpretation "setoid symmetry" 'invert r = (sym ???? r).
+notation ".= r" with precedence 50 for @{'trans $r}.
+interpretation "trans" 'trans r = (trans ????? r).