proposition: Theorem FO_model_equiv_spec (M1 M2 : model) A : FO_model_equiv M1 M2 -> fol_vars A ⊑ ln -> fol_syms A ⊑ ls -> fol_rels A ⊑ lr -> FO_sem M1 A <-> FO_sem M2 A.
proof: Proof. intros H1 H2 H3 H4. destruct M1 as ((s1&r1) & rho1 & G1). destruct M2 as ((s2&r2) & rho2 & G2). simpl in H1 |- *. apply fo_model_projection' with (i := fun x => x) (j := fun x => x) (ls := ls) (lr := lr); auto. + intros s v Hs. replace (vec_map (fun x => x) v) with v; simpl; auto. * apply H1; auto. * apply vec_pos_ext; intro; rew vec. + intros r v Hr. replace (vec_map (fun x => x) v) with v. * apply H1; auto. * apply vec_pos_ext; intro; rew vec. + intros n Hn; apply H1; auto. Qed.
imports: List Arith Bool Lia Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils fol_ops fo_sig fo_terms fo_logic fo_sat decidable)