proposition: Theorem TrueRepeat_G_G1_equiv : Pr[ TrueRepeat_G] == Pr[TrueRepeat_G1].
proof: Proof. unfold TrueRepeat_G, TrueRepeat_G1. inline_first. comp_skip. assert (Pr [b <-$ Repeat (c x) P; ret f b ] == Pr [b <-$ (y <-$ compMap _ (fun _ => (c x)) (forNats n); match (hd_error (filter P y)) with | None => Repeat (c x) P | Some z => ret z end); ret f b ]). comp_skip. eapply Repeat_unroll_n. eauto. eauto. rewrite H0. clear H0. inline_first. comp_skip. case_eq (hd_error (filter P x0)); intuition. comp_irr_r. edestruct Repeat_c_terminating; eauto. eapply well_formed_Repeat. unfold eq_dec. intuition. eapply (EqDec_dec _). eauto. eauto. reflexivity. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndNat FCF.Hybrid