-notation "hbox(a break ⇒ b)" right associative with precedence 20 for @{ 'Imply $a $b }.
-(*
-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).