fact: Definition bij_t (X Y : Type) := { i : X -> Y & { j | (forall x, j (i x) = x) /\ forall y, i (j y) = y } }.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac fin_base fin_choice) Undecidability.Shared.Libs.DLW.Vec(pos vec)