fact: Definition Halt_murec (a : { n : nat & recalg n & Vector.t nat n }) : Prop := let (n, f, v) := a in exists x, [f ; v ] ▹ x.
imports: Arith Lia List Bool Eqdep_dec  Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list finite pos vec)