Les relations familiales sur l'Atelier B

J'ai proposé aux étudiants d'utiliser l'Atelier B. Un (au moins, ouf ! je n'ai pas perdu mon temps) a entré la spec et ses définitions. Il a ajouté l'initialisation. Il a pu "passer le type check". Bien. Mais l'Atelier n'a pu prouver l'initialisation.
Lecture de l'obligation de preuve (Proof Obligation, PO) :
Invariant & Initialisation => {} <: PERSONNE
L'Atelier B écrit même l'invariant et l'initialisation. Partie de l'invariant on trouve que PERSONNE est un ensemble non vide et fini. Il dit tout !

Où est l'erreur ?

SETS
PERSONNE
...
hommes <: PERSONNE &
femmes <: PERSONNE &
hommes \/ femmes = PERSONNE &
hommes /\ femmes = {}

Or dans l'initialisation, on trouve :
hommes := {} || femmes := {}
ce qui fait que
hommes \/ femmes = {}
et que PERSONNE = {}

Mais l'Atelier B connaît la définition des SETS (ensembles finis et NON VIDES)

Il ne peut prouver que PERSONNE est à la fois VIDE et NON VIDE.

Ce n'est pas négociable !

Alors monsieur, on fait quoi ?

SETS
PERSONNE
...
humains <: PERSONNE &
hommes <: PERSONNE &
hommes <: humains &
femmes <: PERSONNE &
femmes <: humains &
hommes \/ femmes = humains &
hommes /\ femmes = {}