fact: Fixpoint Σrem_constants (n : nat) A { struct A } := match A with | ⊥ => ⊥ | fol_atom r v => @fol_atom Σ' r (vec_map (fot_rem_cst n) v) | fol_bin b A B => fol_bin b (Σrem_constants n A) (Σrem_constants n B) | fol_quant q A => fol_quant q (Σrem_constants (S n) A) end.
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)