proposition: Fact fol_sem_lconj lf φ : ⟪fol_lconj lf⟫ φ <-> forall f, f ∊ lf -> ⟪f⟫ φ.
proof: Proof. induction lf as [ | f lf IHlf ]; simpl. + split; tauto. + rewrite IHlf. split. * intros [] ? [ -> | ]; auto. * intros H; split; intros; apply H; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils fol_ops fo_sig fo_terms) Undecidability.Shared.ListAutomation