+ [ constructor 1;
+ [ apply (λU.image ?? t U);
+ | intros; apply (#‡e); ]
+ | constructor 1;
+ [ apply (λU.minus_star_image ?? t U);
+ | intros; apply (#‡e); ]
+ | constructor 1;
+ [ apply (λU.star_image ?? t U);
+ | intros; apply (#‡e); ]
+ | constructor 1;
+ [ apply (λU.minus_image ?? t U);
+ | intros; apply (#‡e); ]
+ | intros; split; intro;
+ [ change in f with (∀a. a ∈ image ?? t p → a ∈ q);
+ change with (∀a:o1. a ∈ p → a ∈ star_image ?? t q);
+ intros 4; apply f; exists; [apply a] split; assumption;
+ | change in f with (∀a:o1. a ∈ p → a ∈ star_image ?? t q);
+ change with (∀a. a ∈ image ?? t p → a ∈ q);
+ intros; cases f1; cases x; clear f1 x; apply (f ? f3); assumption; ]
+ | intros; split; intro;
+ [ change in f with (∀a. a ∈ minus_image ?? t p → a ∈ q);
+ change with (∀a:o2. a ∈ p → a ∈ minus_star_image ?? t q);
+ intros 4; apply f; exists; [apply a] split; assumption;
+ | change in f with (∀a:o2. a ∈ p → a ∈ minus_star_image ?? t q);
+ change with (∀a. a ∈ minus_image ?? t p → a ∈ q);
+ intros; cases f1; cases x; clear f1 x; apply (f ? f3); assumption; ]
+ | intros; split; intro; cases f; clear f;
+ [ cases x; cases x2; clear x x2; exists; [apply w1]
+ [ assumption;
+ | exists; [apply w] split; assumption]
+ | cases x1; cases x2; clear x1 x2; exists; [apply w1]
+ [ exists; [apply w] split; assumption;
+ | assumption; ]]]
+qed.
+
+lemma orelation_of_relation_preserves_equality:
+ ∀o1,o2:REL.∀t,t': arrows1 ? o1 o2. eq1 ? t t' → orelation_of_relation ?? t = orelation_of_relation ?? t'.
+ intros; split; unfold orelation_of_relation; simplify; intro; split; intro;
+ simplify; whd in o1 o2;
+ [ change with (a1 ∈ minus_star_image ?? t a → a1 ∈ minus_star_image ?? t' a);
+ apply (. #‡(e‡#));
+ | change with (a1 ∈ minus_star_image ?? t' a → a1 ∈ minus_star_image ?? t a);
+ apply (. #‡(e ^ -1‡#));
+ | change with (a1 ∈ minus_image ?? t a → a1 ∈ minus_image ?? t' a);
+ apply (. #‡(e‡#));
+ | change with (a1 ∈ minus_image ?? t' a → a1 ∈ minus_image ?? t a);
+ apply (. #‡(e ^ -1‡#));
+ | change with (a1 ∈ image ?? t a → a1 ∈ image ?? t' a);
+ apply (. #‡(e‡#));
+ | change with (a1 ∈ image ?? t' a → a1 ∈ image ?? t a);
+ apply (. #‡(e ^ -1‡#));
+ | change with (a1 ∈ star_image ?? t a → a1 ∈ star_image ?? t' a);
+ apply (. #‡(e‡#));
+ | change with (a1 ∈ star_image ?? t' a → a1 ∈ star_image ?? t a);
+ apply (. #‡(e ^ -1‡#)); ]
+qed.
+
+lemma hint: ∀o1,o2:OA. Type_OF_setoid2 (arrows2 ? o1 o2) → carr2 (arrows2 OA o1 o2).
+ intros; apply t;
+qed.
+coercion hint.
+
+lemma orelation_of_relation_preserves_identity:
+ ∀o1:REL. orelation_of_relation ?? (id1 ? o1) = id2 OA (SUBSETS o1).
+ intros; split; intro; split; whd; intro;
+ [ change with ((∀x. x ♮(id1 REL o1) a1→x∈a) → a1 ∈ a); intros;
+ apply (f a1); change with (a1 = a1); apply refl1;
+ | change with (a1 ∈ a → ∀x. x ♮(id1 REL o1) a1→x∈a); intros;
+ change in f1 with (x = a1); apply (. f1 ^ -1‡#); apply f;
+ | alias symbol "and" = "and_morphism".
+ change with ((∃y: carr o1.a1 ♮(id1 REL o1) y ∧ y∈a) → a1 ∈ a);
+ intro; cases e; clear e; cases x; clear x; change in f with (a1=w);
+ apply (. f^-1‡#); apply f1;
+ | change with (a1 ∈ a → ∃y: carr o1.a1 ♮(id1 REL o1) y ∧ y∈a);
+ intro; exists; [apply a1]; split; [ change with (a1=a1); apply refl1; | apply f]
+ | change with ((∃x: carr o1.x ♮(id1 REL o1) a1∧x∈a) → a1 ∈ a);
+ intro; cases e; clear e; cases x; clear x; change in f with (w=a1);
+ apply (. f‡#); apply f1;
+ | change with (a1 ∈ a → ∃x: carr o1.x ♮(id1 REL o1) a1∧x∈a);
+ intro; exists; [apply a1]; split; [ change with (a1=a1); apply refl1; | apply f]
+ | change with ((∀y.a1 ♮(id1 REL o1) y→y∈a) → a1 ∈ a); intros;
+ apply (f a1); change with (a1 = a1); apply refl1;
+ | change with (a1 ∈ a → ∀y.a1 ♮(id1 REL o1) y→y∈a); intros;
+ change in f1 with (a1 = y); apply (. f1‡#); apply f;]