proposition: Lemma close_extract A phi : A ⊢ close All phi -> A ⊢ phi.
proof: Proof. intros H. assert (Hclosed : closed (close All phi)) by apply close_closed. unfold close in *. destruct (find_bounded phi) as [n Hn]; cbn in *. erewrite <- subst_id with (sigma := fun x => $x) in H. erewrite (@bounded_subst _ _ _ _ _ _ _ (capture_subs n)) in H. 2: exact Hclosed. 3:easy. 2: lia. apply capture_extract in H. rewrite subst_id in H; intuition. unfold capture_subs. 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