+lemma GRealize_to_GRealize_2 : ∀alpha,M,P1,P2,R1,R2.
+ P2 ⊆ P1 → R1 ⊆ R2 → GRealize alpha M P1 R1 → GRealize alpha M P2 R2.
+#alpha #M #P1 #P2 #R1 #R2 #Himpl1 #Himpl2 #H1 #intape #HP
+cases (H1 intape (Himpl1 … HP)) -H1 #k * #outc * #Hloop #H1
+@(ex_intro ?? k) @(ex_intro ?? outc) % /2/
+qed.
+