proposition: Lemma embed_subst' (sigma : nat -> term') phi : embed' phi[sigma] = (embed' phi)[sigma >> embed_t'].
proof: Proof. induction phi in sigma |- *; cbn; trivial. - f_equal. erewrite !Vector.map_map, Vector.map_ext. reflexivity. apply embed_subst_t'. - firstorder congruence. - rewrite IHphi. f_equal. apply subst_ext. intros []; cbn; trivial. unfold funcomp. cbn. unfold funcomp. now destruct (sigma n) as [x|[]]. Qed.
imports: Undecidability.FOL(Syntax.Facts Semantics.Tarski.FullFacts Deduction.FullNDFacts ZF FST) Undecidability.FOL.Sets(Models.Aczel Models.ZF_model ZF minZF FST) Undecidability.FOL.Reductions(PCPb_to_ZF PCPb_to_ZFeq PCPb_to_minZF PCPb_to_minZFeq PCPb_to_ZFD) Lia Undecidability.PCP(PCP) Undecidability(Shared.ListAutomation)