proposition: Lemma Peirce_Fr {ff} Gamma phi psi : Gamma ⊢M @Fr ff (((phi → psi) → phi) → phi).
proof: Proof. eapply IE. apply DNE_Fr. cbn. apply II. eapply IE. { apply Ctx; auto. try_lr. } apply II. eapply IE. { apply Ctx; auto. try_lr. } apply II. eapply IE. apply DNE_Fr. cbn; fold Q. apply II. eapply IE with (phi:= _ → _). { apply Ctx; auto. try_lr. } apply II, Ctx; auto. try_lr. Qed.
imports: List Lia Undecidability(Shared.ListAutomation) Undecidability.FOL(FragmentSyntax)