proposition: Lemma s_proj_fun k p : functional (@s_proj k p).
proof: Proof. intros v x y Hx Hy. red in Hx, Hy. rewrite <- Hx. trivial. Qed.
imports: Arith Lia List Bool Eqdep_dec Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list finite pos vec) Undecidability.MuRec.MuRec