proposition: Lemma dio_rel_rel_iter n x y : 𝔻F n -> 𝔻F x -> 𝔻F y -> 𝔻R (fun ν => rel_iter R (n ν) (x ν) (y ν)).
proof: Proof. Proof using HR. dio by lemma (fun v => rel_iter_seq_equiv R (n v) (x v) (y v)). Defined.
imports: Arith List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list rel_iter sums) Undecidability.H10.Dio(dio_logic dio_expo dio_bounded)