proposition: Lemma nameless_equiv_ex' A phi psi n : bounded_L n A -> bounded n phi -> bounded (S n) psi -> (psi::[p0[↑] | p0 ∈ A]) ⊢ phi[↑] <-> (psi[$n..]::A) ⊢ phi.
proof: Proof. intros HL Hphi Hpsi. split. - intros H % (subst_Weak ($n..)). cbn in *. rewrite map_map, (map_ext _ id), map_id in H. + now rewrite subst_shift in H. + intros. apply subst_shift. - intros H % (subst_Weak (cycle_shift n)). cbn in *. rewrite (map_ext_in _ (subst_form ↑)) in H. + now rewrite cycle_shift_subject, cycle_shift_shift in H. + intros theta HT. now apply cycle_shift_shift, HL. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(FOL.Syntax.Facts FOL.Syntax.Theories) Undecidability(Shared.ListAutomation) Lia