... and now that one is consiserably simplified.
Busy on P_Not case. Done, except for half of the contains_negx_witness lemma.