+ [ intros (R12 R23);
+ constructor 1;
+ constructor 1;
+ [ apply (λs1:A.λs3:C.∃s2:B. s1 ♮R12 s2 ∧ s2 ♮R23 s3);
+ | intros;
+ split; intro; cases H2 (w H3); clear H2; exists; [1,3: apply w ]
+ [ apply (. (H‡#)‡(#‡H1)); assumption
+ | apply (. ((H \sup -1)‡#)‡(#‡(H1 \sup -1))); assumption]]
+ | intros 8; split; intro H2; simplify in H2 ⊢ %;
+ cases H2 (w H3); clear H2; exists [1,3: apply w] cases H3 (H2 H4); clear H3;
+ [ lapply (if ?? (H x w) H2) | lapply (fi ?? (H x w) H2) ]
+ [ lapply (if ?? (H1 w y) H4)| lapply (fi ?? (H1 w y) H4) ]
+ exists; try assumption;
+ split; assumption]
+qed.
+
+definition REL: category1.
+ constructor 1;
+ [ apply setoid
+ | intros (T T1); apply (binary_relation_setoid T T1)
+ | intros; constructor 1;
+ constructor 1; unfold setoid1_of_setoid; simplify;
+ [ intros; apply (c = c1)
+ | intros; split; intro;
+ [ apply (trans ????? (H \sup -1));
+ apply (trans ????? H2);
+ apply H1
+ | apply (trans ????? H);
+ apply (trans ????? H2);
+ apply (H1 \sup -1)]]
+ | apply composition
+ | intros 9;
+ split; intro;
+ cases f (w H); clear f; cases H; clear H;
+ [cases f (w1 H); clear f | cases f1 (w1 H); clear f1]
+ cases H; clear H;
+ exists; try assumption;
+ split; try assumption;
+ exists; try assumption;
+ split; assumption
+ |6,7: intros 5; unfold composition; simplify; split; intro;
+ unfold setoid1_of_setoid in x y; simplify in x y;
+ [1,3: cases H (w H1); clear H; cases H1; clear H1; unfold;
+ [ apply (. (H \sup -1 : eq1 ? w x)‡#); assumption
+ | apply (. #‡(H : eq1 ? w y)); assumption]
+ |2,4: exists; try assumption; split; first [apply refl | assumption]]]
+qed.
+
+definition full_subset: ∀s:REL. Ω \sup s.
+ apply (λs.{x | True});
+ intros; simplify; split; intro; assumption.