proposition: Lemma rm_const_tm_swap { p : peirce } A t s x a : binZF <<= 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. + unfold sshift. asimpl. apply IH; try apply in_hd. 1: intros k Hk; now apply HB,HA. now apply (Weak Hx). + apply ex_equiv. intros C z HC. cbn. apply and_equiv; try tauto. unfold sshift. asimpl. apply IH; try apply in_hd_tl. now rewrite HA, HB. apply (Weak Hx). now rewrite HB. - rewrite (vec_inv1 v). cbn. apply ex_equiv. intros B y HB. cbn. apply and_equiv; try tauto. unfold sshift. asimpl. apply IH; try apply in_hd. now rewrite HA. now apply (Weak Hx). - rewrite (vec_inv1 v). cbn. apply ex_equiv. intros B y HB. cbn. apply and_equiv; try tauto. unfold sshift. asimpl. apply IH; try apply in_hd. now rewrite HA. now apply (Weak Hx). Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Syntax.Asimpl Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.Deduction.FullNDFacts Undecidability.FOL.Sets(binZF ZF) Undecidability.FOL.Reductions.PCPb_to_ZF Undecidability(Shared.ListAutomation) Morphisms Undecidability.FOL(Reductions.PCPb_to_ZFeq)