proposition: Lemma Σunif_one_rel_complete A φ : ⟪A⟫ φ <-> ⟪encode A⟫' φ.
proof: Proof. induction A as [ | r v | | ] in φ |- *; cbn; try tauto. + apply fol_equiv_ext; do 2 f_equal. revert v; generalize (Ha r); rewrite Ha; intros E v. rewrite eq_nat_uniq with (H := E). unfold convert_v; rewrite !cast_refl, vec_map_map. apply vec_pos_ext; intro; rew vec. generalize (vec_pos v p); intros []; simpl; auto; exfalso; auto. + apply fol_bin_sem_ext; auto. + apply fol_quant_sem_ext; intro; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils fol_ops fo_sig fo_terms fo_logic)