fact: Fixpoint Σ2_ΣSSn1 (d : nat) (A : fol_form Σ2) : fol_form (Σn1 (S (S n))) := match A with | ⊥ => ⊥ | fol_atom r v => PSSn1 n (Σrel_var (vec_head v)) (Σrel_var (vec_head (vec_tail v))) | fol_bin b A B => fol_bin b (Σ2_ΣSSn1 d A) (Σ2_ΣSSn1 d B) | fol_quant fol_fa A => ∀ PSSn1 n (S d) 0 ⤑ Σ2_ΣSSn1 (S d) A | fol_quant fol_ex A => ∃ PSSn1 n (S d) 0 ⟑ Σ2_ΣSSn1 (S d) 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)