proposition: Fact is_cipher_of_fun f1 f2 a b : (forall i, i < l -> f1 i = f2 i) -> is_cipher_of f1 a -> is_cipher_of f2 b -> a = b.
proof: Proof. intros H1 (_ & _ & H2) (_ & _ & H3); subst a b. apply msum_ext; intros; f_equal; auto. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)