fact: Definition nat_enum_cls X (R : X -> X -> Prop) := { f : nat -> option X | forall x, exists y n, f n = Some y /\ R y x }.
imports: List Arith Lia Permutation Relations Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_nat)