-(*
-definition relS: ∀o: basic_pair. concr o → Ω \sup (form o) → CProp.
-
-
- apply (λo:basic_pair.λx:concr o.λS: Ω \sup (form o).∃y: form o.y ∈ S ∧
- (* OK: FunClass_2_OF_binary_relation (concr o) (form o) (rel o) x y *)
- ?);
- change in x with (carr1 (setoid1_of_setoid (concr o)));
- apply (FunClass_2_OF_binary_relation ?? (rel ?) x y);
-x ⊩ y);
-
- rel (concr o) o -> binary_relation ...
- rel ? = seotid1_OF_setoid ?
- carr rel ? = Type_OF_objs1 (concr o) ->
- carr (setoid1_of_REL (concr o))
-
-interpretation "basic pair relation for subsets" 'Vdash2 x y = (relS _ x y).
-interpretation "basic pair relation for subsets (non applied)" 'Vdash = (relS _).
+definition relS: ∀o: basic_pair. binary_morphism1 (concr o) (Ω \sup (form o)) CPROP.
+ intros (o); constructor 1;
+ [ apply (λx:concr o.λS: Ω \sup (form o).∃y: form o.y ∈ S ∧ x ⊩ y);
+ (* BUG HERE: WORKAROUND *) apply (concr o);
+ | intros; split; intros; cases H2; exists [1,3: apply w]
+ [ apply (. (#‡H1)‡(H‡#)); assumption
+ | apply (. (#‡H1 \sup -1)‡(H \sup -1‡#)); assumption]]
+qed.
+
+interpretation "basic pair relation for subsets" 'Vdash2 x y = (fun1 ___ (relS _) x y).
+interpretation "basic pair relation for subsets (non applied)" 'Vdash = (fun1 ___ (relS _)).