proposition: Lemma loop_deductive' { p : peirce } phi A : minZFeq' <<= A -> A ⊢ rm_const_fm (embed phi) -> A ⊢ phi.
proof: Proof. intros H1 H2. eapply IE; try apply H2. eapply CE2. eapply Weak; try apply H1. apply loop_deductive. Qed.
imports: Undecidability.FOL(Semantics.Tarski.FullFacts Syntax.Facts Deduction.FullNDFacts) Undecidability.FOL.Sets(ZF minZF) Undecidability.FOL.Reductions(PCPb_to_ZF PCPb_to_minZF PCPb_to_ZFD) Undecidability(Shared.ListAutomation)