Pour pouvoir appliquer un lemme de transitivité avec `apply`, il faut aider Coq car il ne peut pas deviner tout seul la valeur de `Q`, qui n'apparaît pas dans le but / la conclusion du lemme. Pour cela, on utilise la clause `with`. Par exemple : `apply subset_trans with (Q := Q).`.
Définir en Coq un prédicat binaire `eqset : (X -> Prop) -> (X -> Prop) -> Prop` exprimant l'égalité extensionnelle de deux sous-ensembles. Montrer qu'il s'agit d'une relation d'équivalence. Montrer que `subset` est antisymétrique vis-à-vis de `eqset`.
Définir en Coq un prédicat binaire `eqset : (X -> Prop) -> (X -> Prop) -> Prop` exprimant l'égalité extensionnelle de deux sous-ensembles. Montrer qu'il s'agit d'une relation d'équivalence. Montrer que `subset` est antisymétrique (pour l'égalité `eqset`).
