proposition: Fact fol_sem_mforall n A φ : ⟪fol_mquant fol_fa n A⟫ φ <-> forall v : vec X n, ⟪A⟫ (env_vlift φ v).
proof: Proof. revert A φ; induction n as [ | n IHn ]; intros A phi. + split. * intros H v; vec nil v; simpl; auto. * intros H; apply (H ø). + rewrite fol_mquant_S, IHn; split. * intros H v; vec split v with x; apply (H v). * intros H v; intros x; apply (H (x##v)). 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