proposition: Theorem TrueRepeat_G2_G3_equiv : Pr[x <-$ TrueRepeat_G2; ret (fst x || snd x)] <= Pr[x <-$ TrueRepeat_G3; ret (fst x || snd x)].
proof: Proof. unfold TrueRepeat_G2, TrueRepeat_G3. repeat (inline_first; comp_skip). comp_simp. eapply comp_spec_impl_le. eapply comp_spec_ret. simpl. case_eq ( hd_error (filter P x0)); intuition. rewrite orb_false_r in *. eapply fold_left_orb_true_in. eapply filter_In. eapply hd_error_Some_In. eauto. trivial. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndNat FCF.Hybrid