proposition: Lemma embed_ZF' { p : peirce } phi : phi el minZFeq' -> ZFeq' ⊢ embed phi.
proof: Proof. intros [<-|[<-|[<-|[<-|[<-|[<-|[<-|[<-|[<-|[<-|[]]]]]]]]]]]. 1-5: cbn; apply Ctx; unfold ZFeq', ZF'; eauto. - cbn. apply (ExI ∅). cbn. apply ZF_eset. - assert (H : ZFeq' ⊢ ax_pair) by (apply Ctx; unfold ZFeq', ZF'; eauto 7). cbn. prv_all x. prv_all y. apply (ExI ({x; y})). cbn. subsimpl. apply (AllE y) in H. cbn in H. apply (AllE x) in H. cbn in H. now subsimpl_in H. - assert (H : ZFeq' ⊢ ax_union) by (apply Ctx; unfold ZFeq', ZF'; eauto 8). cbn. prv_all x. apply (ExI (⋃ x)). cbn. subsimpl. apply (AllE x H). - assert (H : ZFeq' ⊢ ax_power) by (apply Ctx; unfold ZFeq', ZF'; eauto 9). cbn. prv_all x. apply (ExI (PP x)). cbn. subsimpl. apply (AllE x H). - cbn. apply (ExI ω). cbn. apply CI. + assert (H : ZFeq' ⊢ ax_om1) by (apply Ctx; unfold ZFeq', ZF'; eauto 10). unfold ax_om1 in H. apply (IE (CE1 (ZF_inductive_embed ω))) in H. apply H. + assert (H : ZFeq' ⊢ ax_om2) by (apply Ctx; unfold ZFeq', ZF'; eauto 11). prv_all x. apply II. apply (AllE x) in H. cbn in H. eapply IE; try apply (Weak H); auto. specialize (CE2 (ZF_inductive_embed x)). intros H'. eapply IE; try apply (Weak H'); auto. 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)