proposition: Lemma rm_const_tm_swap { p : peirce } A t s x a : minZFeq' <<= A -> A ⊢ (rm_const_tm t)[x..] -> A ⊢ (rm_const_tm s)[a.:x..] <-> A ⊢ (rm_const_tm s`[t..])[a..].
proof: Proof. induction s in A, a, x |- *; cbn; try destruct F; cbn; intros HA Hx; try tauto. - destruct x0; cbn; try tauto. now apply rm_const_tm_equiv. - rewrite (vec_inv2 v). cbn. apply ex_equiv. intros B y HB. cbn. apply and_equiv. + erewrite !subst_comp, subst_ext. setoid_rewrite subst_ext at 2. apply IH; try apply in_hd. now rewrite HA. now apply (Weak Hx). all: intros [|[]]; cbn; try reflexivity. apply subst_term_shift. + apply ex_equiv. intros C z HC. cbn. apply and_equiv; try tauto. erewrite !subst_comp, subst_ext. setoid_rewrite subst_ext at 2. apply IH; try apply in_hd_tl. now rewrite HA, HB. apply (Weak Hx). now rewrite HB. all: intros [|[]]; cbn; try reflexivity. rewrite !subst_term_comp. now apply subst_term_id. - rewrite (vec_inv1 v). cbn. apply ex_equiv. intros B y HB. cbn. apply and_equiv; try tauto. erewrite !subst_comp, subst_ext. setoid_rewrite subst_ext at 2. apply IH; try apply in_hd. now rewrite HA. now apply (Weak Hx). all: intros [|[]]; cbn; try reflexivity. apply subst_term_shift. - rewrite (vec_inv1 v). cbn. apply ex_equiv. intros B y HB. cbn. apply and_equiv; try tauto. erewrite !subst_comp, subst_ext. setoid_rewrite subst_ext at 2. apply IH; try apply in_hd. now rewrite HA. now apply (Weak Hx). all: intros [|[]]; cbn; try reflexivity. apply subst_term_shift. 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)