proposition: Lemma refutation_prv T phi : T ⊢TC phi <-> (T ⋄ ¬ phi) ⊢TC ⊥.
proof: Proof. Proof using HF HP. split. - intros (A & HA1 & HA2). use_theory (¬ phi :: A). + intros psi [<-|Ha]. 1: now right. left. now apply HA1. + eapply IE. 1: apply Ctx; now left. eapply Weak. 1: apply HA2. intros a Ha; now right. - intros (A & HA1 & HA2) % prv_T_impl. use_theory A. now apply DN. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.FOL(Syntax.Facts Syntax.Theories Syntax.Asimpl) Undecidability(Shared.ListAutomation) Lia EqdepFacts