- [ apply (λp,q. And4 (eq1 ? (or_f_minus_star_ ?? p) (or_f_minus_star_ ?? q))
- (eq1 ? (or_f_minus_ ?? p) (or_f_minus_ ?? q))
- (eq1 ? (or_f_ ?? p) (or_f_ ?? q))
- (eq1 ? (or_f_star_ ?? p) (or_f_star_ ?? q)));
- | whd; simplify; intros; repeat split; intros; apply refl1;
- | whd; simplify; intros; cases H; clear H; split;
- intro a; apply sym; generalize in match a;assumption;
- | whd; simplify; intros; cases H; cases H1; clear H H1; split; intro a;
- [ apply (.= (H2 a)); apply H6;
- | apply (.= (H3 a)); apply H7;
- | apply (.= (H4 a)); apply H8;
- | apply (.= (H5 a)); apply H9;]]]
-qed.
-
-definition or_f_minus_star: ∀P,Q:OAlgebra.ORelation_setoid P Q ⇒ arrows1 SET P Q.
+ (* tenere solo una uguaglianza e usare la proposizione 9.9 per
+ le altre (unicita' degli aggiunti e del simmetrico) *)
+ [ apply (λp,q. And42 (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 a; clear a; split;
+ intro a; apply sym1; generalize in match a;assumption;
+ | whd; simplify; intros; cases a; cases a1; clear a a1; 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.unary_morphism2 (ORelation_setoid P Q) (P ⇒ Q).