Yes.

No. It is the one from multiplication, or rather, it is the one found in expressions such as “Cartesian product” (i.e., tuple). Anyway, that does not change the meaning, you can only `destruct`

something with an inductive type.

An object `S`

of type `U -> Prop`

should be seen as a predicate over `U`

, or equivalently, as the characteristic function of a subset of `U`

. Then, an element `x`

is part of `S`

, if the property `S x`

holds. Suppose `T`

is another object of type `U -> Prop`

. The element `x`

is part of both `S`

and `T`

if it satisfies `S x /\ T x`

. In other words, you can define the predicate characterizing the intersection of `S`

and `T`

as `fun x => S x /\ T x`

(which still has type `U -> Prop`

). More generally, you can define an intersection operator as `fun S T x => S x /\ T x`

, and if you want to make it implicitly generic with respect to `U`

, you get `fun {U} (S T: U -> Prop) x => S x /\ T x`

. The exact same thing can be done to define the union, except that you would replace the conjunction by a disjunction.

The `Ensembles`

library provides all these definitions, but I would recommend against using it, especially if you are a beginner with Coq. (And if you are not a beginner, you do not need it anyway.) I think it would be much more instructive for you to directly manipulate predicates by hand:

```
Definition union {U} (S T : U -> Prop) (x : U) := S x \/ T x.
Definition inter {U} (S T : U -> Prop) (x : U) := S x /\ T x.
Definition empty {U} (x : U) := False.
Definition subset {U} (S T : U -> Prop) := forall x, S x -> T x.
Goal forall U (S T : U -> Prop), subset (union S T) (union T S).
Proof. intros U S T x. unfold union. tauto. Qed.
```