proposition: Lemma rm_const_sat (rho : nat -> V) (phi : form) : rho ⊨ phi <-> rho ⊨ embed (rm_const_fm phi).
proof: Proof. Proof using M_ZF. induction phi in rho |- *; try destruct P; try destruct b0; try destruct q; cbn. 1: firstorder easy. 3-5: specialize (IHphi1 rho); specialize (IHphi2 rho); intuition easy. - rewrite (vec_inv2 t). cbn. split. + intros H. exists (eval rho (Vector.hd t)). rewrite rm_const_tm_sat. split; try reflexivity. exists (eval rho (Vector.hd (Vector.tl t))). now rewrite embed_sshift, sat_sshift1, rm_const_tm_sat. + intros (x & Hx & y & Hy & H). apply rm_const_tm_sat in Hx. change (set_elem (eval rho (Vector.hd t)) (eval rho (Vector.hd (Vector.tl t)))). rewrite embed_sshift, sat_sshift1, rm_const_tm_sat in Hy. now rewrite <- Hx, <- Hy. - rewrite (vec_inv2 t). cbn. split. + intros H. exists (eval rho (Vector.hd t)). rewrite rm_const_tm_sat. split; try reflexivity. exists (eval rho (Vector.hd (Vector.tl t))). rewrite embed_sshift, sat_sshift1, rm_const_tm_sat. split; trivial. reflexivity. + intros (x & Hx & y & Hy & H). apply rm_const_tm_sat in Hx. change (set_equiv (eval rho (Vector.hd t)) (eval rho (Vector.hd (Vector.tl t)))). rewrite embed_sshift, sat_sshift1, rm_const_tm_sat in Hy. now rewrite <- Hx, <- Hy. - split; intros; apply IHphi, H. - firstorder eauto. 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 PCPb_to_ZFeq PCPb_to_minZF) Undecidability(Shared.ListAutomation) Morphisms