record binary_relation (A,B: SET) : Type[1] ≝
{ satisfy:> binary_morphism1 A B CPROP }.
record binary_relation (A,B: SET) : Type[1] ≝
{ satisfy:> binary_morphism1 A B CPROP }.
intros; unfold extS; unfold ext; unfold singleton; simplify;
split; intros 2; simplify; simplify in f;
[ cases f; cases e; cases x1; change in f2 with (x =_1 w); apply (. #‡f2); assumption;
intros; unfold extS; unfold ext; unfold singleton; simplify;
split; intros 2; simplify; simplify in f;
[ cases f; cases e; cases x1; change in f2 with (x =_1 w); apply (. #‡f2); assumption;