proposition: Fact ra_rec_inj k f g f' g' : @ra_rec k f g = ra_rec f' g' -> f = f' /\ g = g'.
proof: Proof. inj; intros; diauto. Qed.
imports: Arith Lia List Bool Eqdep_dec Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list finite pos vec) Undecidability.MuRec.MuRec