Class inequality is strict containment, given inclusion

Assume $\forall L\subseteq B^*,\ L\in P\Rightarrow L\in NP$. Under precisely this inclusion hypothesis, $P\ne NP$ if and only if $P\subsetneq NP$, where the strict inclusion means $P\subseteq NP$ and the reverse inclusion fails. The hypothesis is supplied to the theorem rather than proved by its statement. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length. The set $P$ consists exactly of languages $L\subseteq B^*$ for which there is a Boolean function $\chi:B^*\to B$ satisfying $D(\chi)$ and $\forall w\in B^*,\ w\in L\ \Longleftrightarrow\ \chi(w)=\mathrm{true}$. The set $NP$ consists exactly of languages $L\subseteq B^*$ for which there exist $R:B^*\times B^*\to B$ and $k\in\mathbb N$ satisfying $C(R)$ and $\forall w\in B^*,\ w\in L\ \Longleftrightarrow\ \exists y\in B^*,\ |y|\le |w|^k\ \land\ R(w,y)=\mathrm{true}$. This includes $k=0$ and empty input: $0^0=1$, whereas $0^k=0$ for $k>0$. Write $D(\chi)$ for existence of such a machine and a polynomial $p\in\mathbb N[X]$ that, for every $w\in B^*$, compute the singleton output $[\chi(w)]$ from input $w$ in at most $p(|w|)$ steps. Write $C(R)$ for existence of such a machine and a polynomial $p\in\mathbb N[X]$ that, for all $w,y\in B^*$, compute $[R(w,y)]$ in at most $p(|w|+|y|)$ steps from the list obtained by tagging every bit of $w$ with the left injection into $B\sqcup B$, tagging every bit of $y$ with the right injection, and concatenating those two lists. A machine in these assertions is a Mathlib TM2 stack machine with finitely many stack indices, instruction labels, and control states, a finite input-stack alphabet, designated input and output stacks, a program, and initial label and control state; its other stack alphabets need not be finite. Input and output alphabet bijections transport the specified encoded lists to the corresponding stack alphabets. Computation starts with only the input stack populated, and reaches a halted configuration with the specified output on the output stack, all other stacks empty, and the control state reset to its initial value. Time counts executions of whole TM2 statements, each of which may contain several stack operations.