Added a proof of a existential variable in NK.v

It seemed to be necessary to add a Obligation to the Program Instance nj to instantiate first a BAEA.