apply (. #‡(e‡#)); ]
qed.
-lemma hint: ∀o1,o2:OA. Type_OF_setoid2 (arrows2 ? o1 o2) → carr2 (arrows2 OA o1 o2).
+lemma hint: ∀o1,o2:OA. Type_OF_setoid21 (arrows2 ? o1 o2) → carr2 (arrows2 OA o1 o2).
intros; apply t;
qed.
coercion hint.
| change with (a1 ∈ a → ∀y.a1 ♮(id1 REL o1) y→y∈a); intros;
change in f1 with (a1 = y); apply (. f1^-1‡#); apply f;]
qed.
-
-lemma hint2: ∀S,T. carr2 (arrows2 OA S T) → Type_OF_setoid2 (arrows2 OA S T).
+(*
+lemma hint2: ∀S,T. carr2 (arrows2 OA S T) → Type_OF_setoid21 (arrows2 OA S T).
intros; apply c;
qed.
coercion hint2.
-
+*)
(* CSC: ???? forse un uncertain mancato *)
lemma orelation_of_relation_preserves_composition:
∀o1,o2,o3:REL.∀F: arrows1 ? o1 o2.∀G: arrows1 ? o2 o3.
split; [ assumption | exists; [apply w] split; assumption ]
| cases e; cases x; cases f1; cases x1; clear e x f1 x1; exists; [apply w1 ]
split; [ exists; [apply w] split; assumption | assumption ]
- | cases e; cases x; cases f; cases x1; clear e x f x1; exists; [ apply w1 ]
+ | unfold arrows1_OF_ORelation_setoid;
+ cases e; cases x; cases f; cases x1; clear e x f x1; exists; [ apply w1 ]
split; [ assumption | exists; [apply w] split; assumption ]
- | cases e; cases x; cases f1; cases x1; clear e x f1 x1; exists; [apply w1 ]
+ | unfold arrows1_OF_ORelation_setoid in e;
+ cases e; cases x; cases f1; cases x1; clear e x f1 x1; exists; [apply w1 ]
split; [ exists; [apply w] split; assumption | assumption ]
| whd; intros; apply f; exists; [ apply y] split; assumption;
| cases f1; clear f1; cases x; clear x; apply (f w); assumption;]