proposition: Lemma bwd_sat rho phi : fol_sem M2 rho phi <-> rho ⊨ translate phi.
proof: Proof. induction phi in rho |- *; try destruct p; try destruct f; cbn; try now intuition; try firstorder. - unfold sat. rewrite map_map. erewrite map_ext. 1:{ match goal with [ |- ?P <-> ?Q ] => enough (P = Q) as -> end. 1: reflexivity. reflexivity. } eapply bwd_eval. - split; intros [d H]; exists d; apply IHphi. + eapply fol_sem_ext; try apply H. now intros []. + eapply sat_ext; try apply H. now intros []. - split; intros H d; apply IHphi. + eapply fol_sem_ext; try apply H. now intros []. + eapply sat_ext; try apply H. now intros []. Qed.
imports: Undecidability.FOL(Syntax.Facts Semantics.Tarski.FullFacts Syntax.BinSig Semantics.FiniteTarski.Full) Undecidability.FOL.TRAKHTENBROT(fo_sat fo_sig fo_terms fo_logic fol_ops) Undecidability.Synthetic.DecidabilityFacts Vector Lia