proposition: Lemma Σunif_one_rel_sound A φ : ⟪A⟫ φ <-> ⟪encode A⟫' (convert_env φ).
proof: Proof. induction A as [ | r v | b A HA B HB | [] A HA ] in φ |- *; try tauto. - cbn; rewrite <- (Ha r), !cast_refl. unfold convert_v; rewrite !vec_map_map. apply fol_equiv_ext; f_equal. apply vec_pos_ext; intros p; rew vec. generalize (vec_pos v p). intros [ n | s w ]; simpl; auto; exfalso; auto. - apply fol_bin_sem_ext; auto. - simpl; split. * intros (x & Hx); exists (inl x). revert Hx; rewrite HA; apply fol_sem_ext. intros []; simpl; auto. * intros ( [x | r] & H). + exists x. revert H; rewrite HA; apply fol_sem_ext. intros []; simpl; auto. + exists x0. apply HA; revert H. rewrite <- env_fill_sat. apply fol_sem_ext. intros []; simpl; auto. - simpl; split. * intros H [ x | r ]. + generalize (H x); rewrite HA. apply fol_sem_ext. intros []; simpl; auto. + generalize (H x0). rewrite <- env_fill_sat, HA; apply fol_sem_ext. intros []; simpl; auto. * intros H x. generalize (H (inl x)). rewrite HA; apply fol_sem_ext. intros []; simpl; 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)