proposition: Lemma rm_const_fm_swap { p : peirce } A phi t x : minZFeq' <<= A -> A ⊢ (rm_const_tm t)[x..] -> A ⊢ (rm_const_fm phi)[x..] <-> A ⊢ rm_const_fm phi[t..].
proof: Proof. revert A. induction phi as [| | b0 phi1 IHphi1 phi2 IHphi2| ] using form_ind_subst; cbn; intros A HA Hx. all: try destruct P0; try destruct b0; try destruct q; try tauto. - rewrite (vec_inv2 t0). cbn. apply ex_equiv. cbn. intros B a HB. apply and_equiv. + rewrite subst_comp. erewrite subst_ext. * eapply rm_const_tm_swap. now rewrite HA. now apply (Weak Hx). * intros [|[|]]; trivial. now destruct x as [|[]]. + apply ex_equiv. cbn. intros C a' HC. apply and_equiv; try tauto. rewrite !subst_comp. erewrite subst_ext. setoid_rewrite subst_ext at 2. * eapply rm_const_tm_swap. now rewrite HA, HB. apply (Weak Hx). now rewrite HB. * intros [|[]]; reflexivity. * intros [|[]]; trivial. now destruct x as [|[]]. - rewrite (vec_inv2 t0). cbn. apply ex_equiv. cbn. intros B a HB. apply and_equiv. + rewrite subst_comp. erewrite subst_ext. * eapply rm_const_tm_swap. now rewrite HA. now apply (Weak Hx). * intros [|[|]]; trivial. now destruct x as [|[]]. + apply ex_equiv. cbn. intros C a' HC. apply and_equiv; try tauto. rewrite !subst_comp. erewrite subst_ext. setoid_rewrite subst_ext at 2. * eapply rm_const_tm_swap. now rewrite HA, HB. apply (Weak Hx). now rewrite HB. * intros [|[]]; reflexivity. * intros [|[]]; trivial. now destruct x as [|[]]. - now apply and_equiv; split; (apply IHphi1 + apply IHphi2). - apply or_equiv; intros B HB. + apply IHphi1. now rewrite HA. now apply (Weak Hx). + apply IHphi2. now rewrite HA. now apply (Weak Hx). - apply impl_equiv; intros B HB. + apply IHphi1. now rewrite HA. now apply (Weak Hx). + apply IHphi2. now rewrite HA. now apply (Weak Hx). - apply all_equiv. intros [n|[]]. destruct x as [m|[]]. assert (A ⊢ (rm_const_fm phi[$(S n)..])[$m..] <-> A ⊢ (rm_const_fm phi[$(S n)..][t..])) by now apply H, (Weak Hx). erewrite subst_comp, subst_ext, <- subst_comp, (rm_const_fm_subst ($(S n)..)). setoid_rewrite subst_ext at 2. rewrite H0. erewrite rm_const_fm_subst, !subst_comp, subst_ext. reflexivity. all: intros [|[]]; cbn; try reflexivity. rewrite subst_term_comp, subst_term_id; reflexivity. - apply ex_equiv. intros B s HB. destruct s as [n|[]], x as [m|[]]. assert (B ⊢ (rm_const_fm phi[$(S n)..])[$m..] <-> B ⊢ (rm_const_fm phi[$(S n)..][t..])). { eapply H, (Weak Hx); trivial. now rewrite HA. } erewrite subst_comp, subst_ext, <- subst_comp, (rm_const_fm_subst ($(S n)..)). setoid_rewrite subst_ext at 2. rewrite H0. erewrite rm_const_fm_subst, !subst_comp, subst_ext. reflexivity. all: intros [|[]]; cbn; try reflexivity. rewrite subst_term_comp, subst_term_id; reflexivity. 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)