proposition: Lemma embed_subst (sigma : nat -> term') (phi : form') : 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.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)