proposition: Lemma ExE_named A χ ψ : A ⊢ ∃ χ -> (forall t, (χ[t..]::A) ⊢ ψ) -> A ⊢ ψ.
proof: Proof. intros H1 H2. destruct (nameless_equiv_ex A χ ψ) as [t Ht]. eapply ExE. - eassumption. - apply Ht, H2. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(FOL.Syntax.Facts FOL.Syntax.Theories) Undecidability(Shared.ListAutomation) Lia