fact: Definition surj_t (X Y : Type) := { s : X -> Y | forall y, exists x, y = s x }.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac fin_base fin_choice) Undecidability.Shared.Libs.DLW.Vec(pos vec)