proposition: Lemma nameless_equiv_all' A phi n : bounded_L n A -> bounded (S n) phi -> [f[↑] | f ∈ A] ⊢ phi <-> A ⊢ phi[$n..].
proof: Proof. intros H1 H2. split; intros H. - apply (subst_Weak ($n..)) in H. rewrite map_map in *. erewrite map_ext, map_id in H; try apply H. intros. apply subst_shift. - apply (subst_Weak (cycle_shift n)) in H. rewrite (map_ext_in _ (subst_form ↑)) in H. + now rewrite cycle_shift_subject in H. + intros psi HP. now apply cycle_shift_shift, H1. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.FOL(Syntax.Facts Syntax.Theories Syntax.Asimpl) Undecidability(Shared.ListAutomation) Lia EqdepFacts