[STATEMENT]
lemma second_summands_in_sums: "P y (x \<oplus> y) \<and> P v (z \<oplus> v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P y (x \<oplus> y) \<and> P v (z \<oplus> v)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P y (x \<oplus> y)
 2. P v (z \<oplus> v)
[PROOF STEP]
show "P y (x \<oplus> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P y (x \<oplus> y)
[PROOF STEP]
using second_summand_in_sum
[PROOF STATE]
proof (prove)
using this:
P ?y (?x \<oplus> ?y)

goal (1 subgoal):
 1. P y (x \<oplus> y)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
P y (x \<oplus> y)

goal (1 subgoal):
 1. P v (z \<oplus> v)
[PROOF STEP]
show "P v (z \<oplus> v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P v (z \<oplus> v)
[PROOF STEP]
using second_summand_in_sum
[PROOF STATE]
proof (prove)
using this:
P ?y (?x \<oplus> ?y)

goal (1 subgoal):
 1. P v (z \<oplus> v)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
P v (z \<oplus> v)

goal:
No subgoals!
[PROOF STEP]
qed