proposition: Fact Σ2_list_in_spec l lv ψ : ⟪Σ2_list_in l lv⟫ ψ <-> forall x, x ∊ lv -> ψ x ∈ₘ ψ l.
proof: Proof. unfold Σ2_list_in; rewrite fol_sem_lconj. split. + intros H x Hx. apply (H (_ ∈ _)), in_map_iff. exists x; auto. + intros H f; rewrite in_map_iff. intros (x & <- & ?); apply H; auto. Qed.
imports: List Arith Nat Lia Max Wellfounded Coq.Setoids.Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations fol_ops fo_sig fo_terms fo_logic)