proposition: Theorem ra_rel_fun k (f : recalg k) v x y : [|f|] v x -> [|f|] v y -> x = y.
proof: Proof. revert v x y; change (functional [|f|]). induction f; try (simpl; auto; fail). rewrite ra_rel_fix_comp. apply s_comp_fun; auto. intro; rewrite vec_pos_map; auto. Qed.
imports: Arith Lia List Bool Eqdep_dec Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list finite pos vec) Undecidability.MuRec.MuRec