proposition: Lemma nt_dn_float' {p:peirce} {ff:falsity_flag} A phi: A ⊢ ((¬¬negative_translation phi) → negative_translation phi).
proof: Proof. revert A. induction phi as [| |?[]|?[]]; intros A; cbn. - apply II. eapply IE. 1: apply Ctx; now left. apply II. apply Ctx; now left. - apply II. apply II. eapply IE. 1: apply Ctx; right; now left. apply II. eapply IE. 1: apply Ctx; now left. apply Ctx; right; now left. - apply II. apply II. eapply IE. 1: apply IHphi2. apply II. eapply IE. 1: apply Ctx; right; right; now left. apply II. eapply IE. 1: apply Ctx; right; now left. eapply IE. 1: apply Ctx; now left. apply Ctx; right; right; now left. - apply II. apply AllI. cbn. eapply IE. 1: apply IHphi. apply II. eapply IE. 1: apply Ctx; right; now left. apply II. eapply IE. 1: apply Ctx; right; now left. assert ((negative_translation phi)[up ↑][$0..] = negative_translation phi) as <- by now asimpl. apply AllE. apply Ctx; left; now asimpl. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.FOL(Syntax.Facts Syntax.Theories Syntax.Asimpl) Undecidability(Shared.ListAutomation) Lia EqdepFacts