proposition: Theorem DistMult_G_equiv : forall c, Pr[DM_RC_G6 c] == Pr[DistMult_G _ A1 DM_RC_B2 n c] .
proof: Proof. intuition. unfold DistMult_G, DM_RC_G6, DM_RC_B2. comp_skip. comp_simp. inline_first. comp_skip. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndNat FCF.Hybrid