proposition: Lemma rm_const_sat (rho : nat -> V) (phi : form) : rho ⊨ phi <-> rho ⊨ rm_const_fm phi.
proof: Proof. Proof using VIEQ M_ZF. induction phi as [|b P t|b [] phi1 IH1 phi2 IH2|b [] phi IH] in rho |- *; cbn. - easy. - destruct P; cbn; rewrite (vec_inv2 t); cbn; split. + intros H. exists (eval rho (Vector.hd t)). rewrite rm_const_tm_sat. split; trivial. exists (eval rho (Vector.hd (Vector.tl t))). now rewrite sat_sshift1, rm_const_tm_sat. + intros (x & Hx & y & Hy & H). apply rm_const_tm_sat in Hx as <-. rewrite sat_sshift1, rm_const_tm_sat in Hy. now subst. + intros H. exists (eval rho (Vector.hd t)). rewrite rm_const_tm_sat. split; trivial. exists (eval rho (Vector.hd (Vector.tl t))). now rewrite sat_sshift1, rm_const_tm_sat. + intros (x & Hx & y & Hy & H). apply rm_const_tm_sat in Hx as <-. rewrite sat_sshift1, rm_const_tm_sat in Hy. now subst. - specialize (IH1 rho). specialize (IH2 rho). tauto. - specialize (IH1 rho). specialize (IH2 rho). tauto. - specialize (IH1 rho). specialize (IH2 rho). tauto. - now split; intros; apply IH. - split; intros [? ?]; eexists; apply IH; eassumption. 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)