fact: Fixpoint Σ2_Σn (A : fol_form Σ2) : fol_form Σn := match A with | ⊥ => ⊥ | fol_atom _ v => let x := Σrel_var (vec_head v) in let y := Σrel_var (vec_head (vec_tail v)) in @fol_atom Σn tt (£x##vec_set_pos (fun _ => £y)) | fol_bin b A B => fol_bin b (Σ2_Σn A) (Σ2_Σn B) | fol_quant q A => fol_quant q (Σ2_Σ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 fol_ops fo_sig fo_terms fo_logic fo_sat)