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