proposition: Lemma capture_extract n A phi : A ⊢ subst_form (capture_subs n) (capture All n phi) -> A ⊢ subst_form (capture_subs 0) phi.
proof: Proof. induction n; comp; intuition. apply IHn. apply (AllE (var n)) in H. rewrite subst_comp in H. erewrite subst_ext. 1: apply H. intros [| x]; unfold capture_subs; cbn; f_equal; lia. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.FOL(Syntax.Facts Syntax.Theories Syntax.Asimpl) Undecidability(Shared.ListAutomation) Lia EqdepFacts