qed.
*)
-lemma hint: ∀U. carr U → Type_OF_setoid1 ?(*(setoid1_of_SET U)*).
- [ apply setoid1_of_SET; apply U
- | intros; apply c;]
-qed.
-coercion hint.
-
(* the same as ⋄ for a basic pair *)
definition image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) (Ω \sup V).
intros; constructor 1;
| cases x1; cases x2; clear x1 x2; exists; [apply w1]
[ exists; [apply w] split; assumption;
| assumption; ]]]
-qed. (*sistemare anche l'hint da un'altra parte *)
+qed.