[STATEMENT]
lemma outs'_restrict_gpv: "outs'_gpv (restrict_gpv gpv) \<subseteq> outs_\<I> \<I>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. outs'_gpv (local.restrict_gpv gpv) \<subseteq> outs_\<I> \<I>
[PROOF STEP]
by(blast intro: in_outs'_restrict_gpvD)