proposition: Theorem G3_TrueMult_equiv : Pr[x <-$ TrueRepeat_G3; ret (fst x)] == Pr[TrueMult_G _ c A1 f n].
proof: Proof. unfold TrueRepeat_G3, TrueMult_G. inline_first. comp_skip. inline_first. comp_skip. inline_first. comp_irr_l. edestruct Repeat_c_terminating; eauto. eapply well_formed_Repeat. unfold eq_dec; intuition. eapply (EqDec_dec _). eauto. eauto. simpl. intuition. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndNat FCF.Hybrid