fact: Variable (R : nat -> nat -> Prop) (HR : 𝔻R (fun ν => R (ν 1) (ν 0))).
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)