proposition: Fact fo_proj_simul : fo_projection -> fo_simulation.
proof: Proof. intros [ i j E Hs Hr ]. exists (fun x y => i x = y); auto. + intros s v w H1 H2; rewrite Hs; auto. f_equal; apply vec_pos_ext; intro; rew vec. + intros s v w H1 H2; rewrite Hr; auto. apply fol_equiv_ext; f_equal. apply vec_pos_ext; intro; rew vec. + intros x; exists (i x); auto. + intros y; exists (j y); auto. Defined.
imports: List Arith Lia 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) Undecidability.Shared.ListAutomation