fact: Variable (b c : nat-> nat) (cb cc : nat) (Hb : is_cipher_of b cb) (Hc : is_cipher_of c cc).
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)