-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)));
-##| nnormalize; #x; #a; napply (f_ok … x); napply refl
- | nnormalize; #x; #y; #H; #a; napply sym; napply H
- | nnormalize; #z; #x; #y; #H1; #H2; #a;
- napply trans; ##[##2: napply H1 | ##skip | napply H2]##]
-nqed.
+interpretation "setoid symmetry" 'invert r = (sym ???? r).
+notation ".= r" with precedence 50 for @{'trans $r}.
+interpretation "trans" 'trans r = (trans ????? r).