proposition: Theorem DistSingle_G3_c1_equiv : Pr[DistSingle_G2 c1] == Pr[DistSingle_G3_c1].
proof: Proof. unfold DistSingle_G2, DistSingle_G3_c1. comp_swap_r. comp_skip. comp_simp. comp_skip. epose proof hybrid_replace_c1_equiv as HH. comp_skip. eapply HH. eapply RndNat_support_lt; intuition. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndNat FCF.Hybrid