proposition: Lemma intuitionistic_is_classical {ff:falsity_flag} A phi : A ⊢I phi -> A ⊢C phi.
proof: Proof. induction 1; comp. - now apply II, IHprv. - now eapply IE, IHprv2. - now eapply AllI, IHprv. - now eapply AllE, IHprv. - now eapply Exp, IHprv. - now eapply Ctx, H. - apply Pc. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FragmentFacts Undecidability.FOL.Deduction.FragmentND Undecidability(Shared.ListAutomation) Vector Lia