proposition: Theorem PedersenHiding_G0_equiv : Pr[HidingCommit_G PedersenSetup PedersenCommit A1 A2] == Pr[PedersenHiding_G0].
proof: Proof. unfold HidingCommit_G, PedersenSetup, PedersenCommit, PedersenHiding_G0. repeat (inline_first; comp_skip; comp_simp). Qed.
imports: FCF GroupTheory OTP RndNat RndGrpElem