proposition: Lemma minZF_decomp { p : peirce } phi : minZFeq ⊢T phi -> exists A B, ((map ax_sep' A ++ map ax_rep' B) ++ minZFeq') ⊢ phi.
proof: Proof. intros [C [H1 H2]]. induction C in phi, H1, H2 |- *. - exists nil, nil. cbn. eapply Weak; eauto. - rewrite <- imps in H2. apply IHC in H2 as [A[B HAB]]; auto. rewrite imps in HAB. destruct (H1 a); auto. + exists A, B. eapply Weak; try apply HAB. auto. + exists (phi0 :: A), B. cbn. apply HAB. + exists A, (phi0 :: B). cbn. eapply Weak; try apply HAB. intros psi [->|[[H|H] % in_app_iff|H] % in_app_iff]; auto. apply in_app_iff. left. apply in_app_iff. right. now right. 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)