proposition: Theorem dio_rel_Code l q a : 𝔻F l -> 𝔻F q -> 𝔻F a -> 𝔻R (fun v => Code (l v) (q v) (a v)).
proof: Proof. dio by lemma (fun v => Code_dio (l v) (q v) (a v)). Defined.
imports: Arith List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums bool_nat) Undecidability.H10.Matija(cipher) Undecidability.H10.Dio(dio_logic dio_expo dio_binary)