proposition: Fact fol_sem_ext φ ψ A : (forall n, n ∊ fol_vars A -> φ n = ψ n) -> ⟪A⟫ φ <-> ⟪A⟫ ψ.
proof: Proof. intros H; revert A φ ψ H. induction A as [ | p v | b A IHA B IHB | q A IHA ]; simpl; intros phi psy H; try tauto. + fol equiv rel. apply vec_map_ext; intros w Hw. apply fo_term_sem_ext; auto. intros n Hn; apply H, in_flat_map; exists w; split; auto. apply in_vec_list; auto. + apply fol_bin_sem_ext. * apply IHA; intros; apply H, in_or_app; auto. * apply IHB; intros; apply H, in_or_app; auto. + apply fol_quant_sem_ext. intros x; apply IHA. intros [ | n] Hn; simpl; auto; apply H, in_flat_map. exists (S n); simpl; auto. Qed.
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