proposition: Theorem RPG_G_1_2_eq_until_bad : forall a : bool, evalDist RPS_G_1 (a, false) == evalDist RPS_G_2 (a, false).
proof: Proof. intuition. unfold RPS_G_1, RPS_G_2. eapply comp_spec_impl_eq. comp_skip. eapply rf_rp_oc_eq_until_bad. intuition. simpl in *. intuition. destruct b. simpl in *. destruct p; simpl in *. eapply comp_spec_ret; intuition. pairInv. subst. intuition. subst. intuition. subst. pairInv. intuition. subst. trivial. Qed.
imports: FCF PRF RndInList