fact: Fixpoint Σ0_Σ (A : fol_form (Σ0 Σ)) := match A with | ⊥ => ⊥ | fol_atom r _ => @fol_atom Σ r (cast vec_nil (eq_sym (HΣ r))) | fol_bin b A B => fol_bin b (Σ0_Σ A) (Σ0_Σ B) | fol_quant q A => fol_quant q (Σ0_Σ A) end.
imports: List Arith Lia 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)