proposition: Theorem ElGamal_G1_DDH1 : Pr [G1] == Pr [DDH1 B].
proof: Proof. unfold G1, DDH1, DiffieHellman.DDH1, B, RndGrpElem. inline_first. comp_skip. inline_first. comp_skip. comp_at comp_inline rightc 1%nat. comp_swap rightc. comp_skip. destruct x1. destruct p. comp_at dist_inline leftc 1%nat. comp_at dist_inline leftc 1%nat. comp_swap leftc. comp_skip. comp_inline rightc. comp_skip. inline_first. comp_skip. comp_simp. intuition. Qed.
imports: FCF RndGrpElem Encryption_PK DiffieHellman OTP