proposition: Lemma rm_const_tm_sat (rho : nat -> V) (t : term) x : (x .: rho) ⊨ rm_const_tm t <-> x = eval rho t.
proof: Proof. Proof using VIEQ M_ZF. induction t in x |- *; try destruct F; cbn; split; try intros ->; try rewrite (vec_inv1 v); try rewrite (vec_inv2 v); cbn. - now rewrite VIEQ. - now rewrite VIEQ. - rewrite (vec_nil_eq (Vector.map (eval rho) v)). intros H. apply M_ext; trivial; intros y Hy; exfalso. + firstorder easy. + now apply M_eset in Hy. - rewrite (vec_nil_eq (Vector.map (eval rho) v)). intros d. now apply M_eset. - intros (y & Hy & z & Hz & H). rewrite sat_sshift1, IH in Hy; try apply in_hd. subst. rewrite sat_sshift2, IH in Hz; try apply in_hd_tl. subst. apply M_ext; trivial. + intros a Ha % H. rewrite !VIEQ in Ha. now apply M_pair. + intros a Ha % M_pair; trivial. apply H. now rewrite !VIEQ. - exists (eval rho (Vector.hd v)). rewrite sat_sshift1, IH; try apply in_hd. split; trivial. exists (eval rho (Vector.hd (Vector.tl v))). rewrite sat_sshift2, IH; try apply in_hd_tl. split; trivial. intros d. rewrite !VIEQ. now apply M_pair. - intros (y & Hy & H). rewrite sat_sshift1, IH in Hy; try apply in_hd. subst. apply M_ext; trivial. + intros y Hy % H. now apply M_union. + intros y Hy % M_union; trivial. now apply H. - exists (eval rho (Vector.hd v)). rewrite sat_sshift1, IH; try apply in_hd. split; trivial. intros d. now apply M_union. - intros (y & Hy & H). rewrite sat_sshift1, IH in Hy; try apply in_hd. subst. apply M_ext; trivial. + intros y Hy. now apply M_power, H. + intros y Hy. now apply H, M_power. - exists (eval rho (Vector.hd v)). rewrite sat_sshift1, IH; try apply in_hd. split; trivial. intros d. now apply M_power. - rewrite (vec_nil_eq (Vector.map (eval rho) v)). intros [H1 H2]. apply M_ext; trivial. + apply H2. apply (inductive_sat_om rho). + apply M_om2; trivial. apply inductive_sat with rho. apply H1. - rewrite (vec_nil_eq (Vector.map (eval rho) v)). split. + apply (inductive_sat_om rho). + intros d Hd. apply M_om2; trivial. apply inductive_sat with rho. apply Hd. 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)