After `constructor` on the conjunction goal, two subgoals remain (P and Q) and the proof is not completed.