proposition: Fact fin_t_equiv X (P Q : X -> Prop) : (forall x, P x <-> Q x) -> fin_t P -> fin_t Q.
proof: Proof. intros H (l & Hl); exists l. intro; rewrite <- H, Hl; tauto. Qed.
imports: List Arith Lia Eqdep_dec Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat) Undecidability.Shared.Libs.DLW.Vec(pos vec)