fact: Fixpoint Σ_finite_rev (A : fol_form Σ') : fol_form Σ := match A with | ⊥ => ⊥ | fol_atom r v => fol_atom (proj1_sig r) (vec_map fo_term_fin_rev v) | fol_bin b A B => fol_bin b (Σ_finite_rev A) (Σ_finite_rev B) | fol_quant q A => fol_quant q (Σ_finite_rev A) end.
imports: List Arith Bool Lia Eqdep_dec Max Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils decidable fol_ops fo_sig fo_terms fo_logic fo_sat)