proposition: Lemma combinations_eq T B C x y : HFeq <<= T -> T ⊢ x ≡ enc_stack C -> T ⊢ combinations B x y -> T ⊢ y ≡ enc_stack (derivation_step B C).
proof: Proof. induction B as [|[s t] B IH] in y, T |-*; cbn; intros HT H1 H2; trivial. use_exists H2 u. assert1 H. use_exists H v. clear H. rewrite !combinations_subst, !is_rep_subst. cbn. subsimpl. eapply HF_trans'. auto. eapply CE1. eapply CE1. auto. eapply HF_trans'. auto. 2: apply enc_stack_app; auto. apply HF_eq_bunion; auto. - eapply is_rep_eq; auto. apply (Weak H1); auto. eapply CE2. auto. - apply IH; auto. + apply (Weak H1); auto. + eapply CE2. eapply CE1. auto. Qed.
imports: Undecidability.FOL.ZF Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.Sets.ZF Undecidability.FOL.Reductions.PCPb_to_HF Undecidability.PCP(PCP Util.PCP_facts Reductions.PCPb_iff_dPCPb) Undecidability(Shared.ListAutomation)