proposition: Fact subst_exist_sat2 {ff : falsity_flag} N : forall rho phi, rho ⊨ (exist_times N phi) -> (exists sigma, sigma ⊨ phi).
proof: Proof. induction N. - eauto. - intros rho phi [? H]. now apply IHN in H. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullCore Undecidability(Shared.ListAutomation) Vector Lia