proposition: Lemma nt_Cprv_to_Iprv {p1 : peirce} {ff:falsity_flag} A phi : A ⊢C phi -> (map negative_translation A) ⊢ (negative_translation phi).
proof: Proof. remember class as p2. induction 1; cbn in *. all: try specialize (IHprv Heqp2). all: try specialize (IHprv1 Heqp2). all: try specialize (IHprv2 Heqp2). - eapply II. now apply IHprv. - eapply IE. 1: apply IHprv1. apply IHprv2. - eapply AllI. rewrite map_map in *. erewrite map_ext. 1: apply IHprv. intros a; cbn. now rewrite nt_subst. - rewrite nt_subst. eapply AllE. apply IHprv. - eapply Exp. apply IHprv. - eapply Ctx. now apply in_map. - apply nt_peirce. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.FOL(Syntax.Facts Syntax.Theories Syntax.Asimpl) Undecidability(Shared.ListAutomation) Lia EqdepFacts