(* ∃ is not yet a morphism apply (λX,S,r,F.{x ∈ X | ∃a. a ∈ F ∧ x ♮r a});*)
intros (X S r); constructor 1;
[ intro F; constructor 1; constructor 1;
[ apply (λx. x ∈ X ∧ ∃a:S. a ∈ F ∧ x ♮r a);
| intros; split; intro; cases f (H1 H2); clear f; split;
(* ∃ is not yet a morphism apply (λX,S,r,F.{x ∈ X | ∃a. a ∈ F ∧ x ♮r a});*)
intros (X S r); constructor 1;
[ intro F; constructor 1; constructor 1;
[ apply (λx. x ∈ X ∧ ∃a:S. a ∈ F ∧ x ♮r a);
| intros; split; intro; cases f (H1 H2); clear f; split;