\left[\forall_{{_{-}a} \in \{1~\ldotp \ldotp~t\}}~\left(\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
& & \qout{\lvert m \rangle_{t}~\mbox{part}~{_{-}a}~\mbox{on}~\{1~\ldotp \ldotp~t\}}
} \end{array} \neq \begin{array}{c} \Qcircuit@C=1em @R=.7em{
& & \qout{\lvert n \rangle_{t}~\mbox{part}~{_{-}a}~\mbox{on}~\{1~\ldotp \ldotp~t\}}
} \end{array}\right) \in \mathbb{B}\right)\right] \Rightarrow \left(\left(\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
& & \qout{\lvert m \rangle_{t}~\mbox{part}~1~\mbox{on}~\{1~\ldotp \ldotp~t\}}
} \end{array} \neq \begin{array}{c} \Qcircuit@C=1em @R=.7em{
& & \qout{\lvert n \rangle_{t}~\mbox{part}~1~\mbox{on}~\{1~\ldotp \ldotp~t\}}
} \end{array}\right) \in \mathbb{B}\right) \land \left(\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
& & \qout{\lvert m \rangle_{t}~\mbox{part}~2~\mbox{on}~\{1~\ldotp \ldotp~t\}}
} \end{array} \neq \begin{array}{c} \Qcircuit@C=1em @R=.7em{
& & \qout{\lvert n \rangle_{t}~\mbox{part}~2~\mbox{on}~\{1~\ldotp \ldotp~t\}}
} \end{array}\right) \in \mathbb{B}\right) \land \ldots \land \left(\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
& & \qout{\lvert m \rangle_{t}~\mbox{part}~t~\mbox{on}~\{1~\ldotp \ldotp~t\}}
} \end{array} \neq \begin{array}{c} \Qcircuit@C=1em @R=.7em{
& & \qout{\lvert n \rangle_{t}~\mbox{part}~t~\mbox{on}~\{1~\ldotp \ldotp~t\}}
} \end{array}\right) \in \mathbb{B}\right)\right)