proposition: Lemma AllI_named (A : list form) (phi : form) : (forall t, A ⊢ phi[t..]) -> A ⊢ ∀phi.
proof: Proof. intros H. apply AllI. destruct (nameless_equiv_all A phi) as [t Ht]. apply Ht, H. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.FOL(Syntax.Facts Syntax.Theories Syntax.Asimpl) Undecidability(Shared.ListAutomation) Lia EqdepFacts