Pattern matching with 2 existential quantifiers in Isar

gistfile1.txt

lemma "∃ x. x + 1 = 3" (is "∃ x. ?P x")
proof
  show "?P 2" by simp
qed

(*
lemma "∃ x y. x + y + 1 = 3" (is "∃ x y. ?P x y")
proof
(*
Failed to refine any pending goal 
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
  1 + 1 + 1 = 3
*)
  show "?P 1 1" by simp
qed
*)

lemma "∃ x y. x + y + 1 = 3" (is "∃ x. ?P x")
proof
  show "?P 1" (is "∃ y. ?Q y")
  proof
    show "?Q 1" by simp
  qed
qed