fact: Fixpoint μ_rec n := match n with | 0 => F | S n => fun x => exists y, μ_rec n y /\ G n y x end.
imports: Arith Lia List Bool Eqdep_dec Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list finite pos vec) Undecidability.MuRec.MuRec