+lemma hint1 : ∀P,Q. ORelation_setoid P Q → arrows1 SET P Q. intros; apply (or_f ?? c);qed.
+coercion hint1.
+
+lemma hint3 : ∀P,Q. arrows1 SET P Q → P ⇒ Q. intros; apply c;qed.
+coercion hint3.
+
+lemma hint2: OAlgebra → setoid. intros; apply (oa_P o). qed.
+coercion hint2.
+
+definition or_f_minus_star2: ∀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_f2: ∀P,Q:OAlgebra.ORelation_setoid P Q ⇒ arrows1 SET P Q.
+ intros; constructor 1;
+ [ apply or_f;
+ | intros; cases H; assumption]
+qed.
+
+definition or_f_minus2: ∀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_star2: ∀P,Q:OAlgebra.ORelation_setoid P Q ⇒ arrows1 SET Q P.
+ intros; constructor 1;
+ [ apply or_f_star;
+ | intros; cases H; assumption]
+qed.
+
+interpretation "o-relation f⎻* 2" 'OR_f_minus_star r = (fun_1 __ (or_f_minus_star2 _ _) r).
+interpretation "o-relation f⎻ 2" 'OR_f_minus r = (fun_1 __ (or_f_minus2 _ _) r).
+interpretation "o-relation f* 2" 'OR_f_star r = (fun_1 __ (or_f_star2 _ _) r).
+coercion or_f2.