proposition: Corollary dio_rel_fall_lt_bound a (R : nat -> nat -> (nat -> nat) -> Prop) : 𝔻F a -> 𝔻R (fun ν => R (ν 0) (a ν⭳) ν⭳) -> 𝔻R (fun ν => forall x, x < a ν -> R x (a ν) ν).
proof: Proof. intros; dio auto. Defined.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list sums bounded_quantification) Undecidability.H10.Matija(cipher) Undecidability.H10.Dio(dio_logic dio_cipher dio_elem)