proposition: Theorem TrueRepeat_G1_G2_equiv : Pr [TrueRepeat_G1] <= Pr[x <-$ TrueRepeat_G2; ret (fst x || snd x)].
proof: Proof. unfold TrueRepeat_G1, TrueRepeat_G2. repeat (inline_first; comp_skip). destruct (hd_error (filter P x0)). comp_simp. dist_compute. rewrite e in n0. simpl in *. intuition. eapply rat0_le_all. comp_simp. dist_compute. rewrite e in n0. simpl in *. intuition. eapply rat0_le_all. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndNat FCF.Hybrid