fact: Definition s_comp f gj : natfun i := fun v x => exists gl, f gl x /\ forall p, vec_pos gj p v (vec_pos gl p).
imports: Arith Lia List Bool Eqdep_dec Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list finite pos vec) Undecidability.MuRec.MuRec