proposition: Theorem ElGamal_G1_G2 : Pr[G1] == Pr[G2].
proof: Proof. unfold G1, G2, B. eapply comp_spec_eq_impl_eq. do 3 comp_skip. prog_at comp_swap rightc 1%nat. comp_swap_r. comp_skip. eapply comp_spec_symm. comp_skip. eapply group_OTP_r. subst. eapply comp_spec_consequence. eapply comp_spec_eq_refl. intuition. Qed.
imports: FCF RndGrpElem Encryption_PK DiffieHellman OTP