proposition: Lemma nameless_equiv_all A phi : { t : term | map (subst_form ↑) A ⊢ phi <-> A ⊢ phi[t..] }.
proof: Proof. destruct (find_bounded_L (phi::A)) as [n H]. exists $n. apply nameless_equiv_all'. - intros ? ?. apply H. auto. - eapply bounded_up; try apply H; auto. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(FOL.Syntax.Facts FOL.Syntax.Theories) Undecidability(Shared.ListAutomation) Lia