proposition: Lemma minZF_Leibniz { p : peirce } A (phi : form') x y : minZFeq' <<= A -> A ⊢ x ≡' y -> A ⊢ phi[x..] <-> A ⊢ phi[y..].
proof: Proof. revert A. induction phi using form_ind_subst; cbn; intros A HA HXY; try tauto. - destruct P0; rewrite (vec_inv2 t); cbn; split. + apply minZF_elem; trivial; now apply minZF_Leibniz_tm. + apply minZF_sym in HXY; trivial. apply minZF_elem; trivial; now apply minZF_Leibniz_tm. + intros H. eapply minZF_trans; trivial. apply minZF_Leibniz_tm; trivial. eapply minZF_sym; eauto. eapply minZF_trans; trivial. apply H. now apply minZF_Leibniz_tm. + intros H. eapply minZF_trans; trivial. apply minZF_Leibniz_tm; eauto. eapply minZF_trans; trivial. apply H. apply minZF_Leibniz_tm; trivial. now apply minZF_sym. - destruct b0. + apply and_equiv; firstorder easy. + apply or_equiv; intros B HB. * apply IHphi1. now rewrite HA. now apply (Weak HXY). * apply IHphi2. now rewrite HA. now apply (Weak HXY). + apply impl_equiv; intros B HB. * apply IHphi1. now rewrite HA. now apply (Weak HXY). * apply IHphi2. now rewrite HA. now apply (Weak HXY). - destruct x as [n|[]], y as [m|[]]. destruct q. + apply all_equiv. intros [k|[]]. specialize (H ($(S k)..) A HA HXY). erewrite !subst_comp, subst_ext, <- subst_comp. rewrite H. erewrite !subst_comp, subst_ext. reflexivity. all: now intros [|[]]; cbn. + apply ex_equiv. intros B [k|[]] HB. cbn. specialize (H ($(S k)..) B). erewrite !subst_comp, subst_ext, <- subst_comp. rewrite H. 2: now rewrite HA. 2: now apply (Weak HXY). erewrite !subst_comp, subst_ext. reflexivity. all: now intros [|[]]; cbn. Qed.
imports: Undecidability.FOL.ZF Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.Sets(minZF ZF) Undecidability.FOL.Sets.ZF Undecidability.FOL.Reductions.PCPb_to_ZF Undecidability(Shared.ListAutomation)