proposition: Lemma elem_prv T phi : phi ∈ T -> T ⊢T phi.
proof: Proof. intros ?. use_theory [phi]. 2:apply Ctx; now left. intros psi [->|[]]. apply H. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.FOL(Syntax.Facts Syntax.Theories Syntax.Asimpl) Undecidability(Shared.ListAutomation) Lia EqdepFacts