+ (* tenere solo una uguaglianza e usare la proposizione 9.9 per
+ le altre (unicita' degli aggiunti e del simmetrico) *)
+ [ apply (λp,q. And4 (eq2 ? (or_f_minus_star_ ?? p) (or_f_minus_star_ ?? q))
+ (eq2 ? (or_f_minus_ ?? p) (or_f_minus_ ?? q))
+ (eq2 ? (or_f_ ?? p) (or_f_ ?? q))
+ (eq2 ? (or_f_star_ ?? p) (or_f_star_ ?? q)));
+ | whd; simplify; intros; repeat split; intros; apply refl2;
+ | whd; simplify; intros; cases H; clear H; split;
+ intro a; apply sym1; generalize in match a;assumption;
+ | whd; simplify; intros; cases H; cases H1; clear H H1; split; intro a;
+ [ apply (.= (e a)); apply e4;
+ | apply (.= (e1 a)); apply e5;
+ | apply (.= (e2 a)); apply e6;
+ | apply (.= (e3 a)); apply e7;]]]
+qed.
+
+definition or_f_minus_star: ∀P,Q:OAlgebra.ORelation_setoid P Q ⇒ arrows1 SET P Q.
+ intros; constructor 1;
+ [ apply or_f_minus_star_;
+ | intros; cases H; assumption]
+qed.
+
+definition or_f: ∀P,Q:OAlgebra.ORelation_setoid P Q ⇒ arrows1 SET P Q.
+ intros; constructor 1;
+ [ apply or_f_;
+ | intros; cases H; assumption]
+qed.
+
+coercion or_f.
+
+definition or_f_minus: ∀P,Q:OAlgebra.ORelation_setoid P Q ⇒ arrows1 SET Q P.
+ intros; constructor 1;
+ [ apply or_f_minus_;
+ | intros; cases H; assumption]
+qed.
+
+definition or_f_star: ∀P,Q:OAlgebra.ORelation_setoid P Q ⇒ arrows1 SET Q P.
+ intros; constructor 1;
+ [ apply or_f_star_;
+ | intros; cases H; assumption]
+qed.
+
+lemma arrows1_OF_ORelation_setoid : ∀P,Q. ORelation_setoid P Q → arrows1 SET P Q.
+intros; apply (or_f ?? c);
+qed.
+
+coercion arrows1_OF_ORelation_setoid nocomposites.
+
+lemma umorphism_OF_ORelation_setoid : ∀P,Q. ORelation_setoid P Q → P ⇒ Q.
+intros; apply (or_f ?? c);
+qed.
+
+coercion umorphism_OF_ORelation_setoid.
+
+
+lemma uncurry_arrows : ∀B,C. arrows1 SET B C → B → C.
+intros; apply ((fun_1 ?? c) t);
+qed.