proposition: Lemma nt_Cprv_equiv A phi : A ⊢C phi <-> A ⊢C (negative_translation phi).
proof: Proof. revert A. induction phi as [| |[]|[]] using form_ind_falsity; intros A; cbn; split; intros Hprv. - easy. - easy. - eapply DN_into. easy. - eapply DN. easy. - apply II. apply IHphi2. eapply IE. 1: eapply Weak; [apply Hprv|firstorder]. apply IHphi1. apply Ctx; now left. - apply II. apply IHphi2. eapply IE. 1: eapply Weak; [apply Hprv|firstorder]. apply IHphi1. apply Ctx; now left. - apply (subst_Weak ↑) in Hprv. asimpl in Hprv. eapply (AllE $0) in Hprv. asimpl in Hprv. apply AllI. apply IHphi. apply Hprv. - apply (subst_Weak ↑) in Hprv. asimpl in Hprv. eapply (AllE $0) in Hprv. asimpl in Hprv. apply AllI. apply IHphi. apply Hprv. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.FOL(Syntax.Facts Syntax.Theories Syntax.Asimpl) Undecidability(Shared.ListAutomation) Lia EqdepFacts