proposition: Corollary dio_rel_fall_le a (R : nat -> (nat -> nat) -> Prop) : 𝔻F a -> 𝔻R (fun ν => R (ν 0) ν⭳) -> 𝔻R (fun ν => forall x, x <= a ν -> R x ν).
proof: Proof. intros Ha HK. by dio equiv (fun v => forall x, x < 1+a v -> R x v). abstract (intros v; split; intros H x Hx; apply H; lia). 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)