proposition: Theorem DistSingle_G2_equiv : forall c, Pr[DistSingle_G1 c] == Pr[DistSingle_G2 c].
proof: Proof. intuition. unfold DistSingle_G1, DistSingle_G2. unfold B1, B2. inline_first. comp_skip. comp_simp. comp_swap_l. comp_skip. inline_first. comp_skip. comp_inline_r. comp_skip. comp_simp. intuition. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndNat FCF.Hybrid