Correctness of existential prefix merging

Moving a relation quantifier across an independent operand preserves truth. Relation renaming prevents capture and preserves the matrices and their sizes.

theorem Complexity.DescriptiveComplexity.size_mergeExist_internal {V : Vocabulary} (isConjunction : Bool) {rctx : List Nat} {n : Nat} (φ ψ : SOFormula V rctx n) : (SOFormula.mergeExist isConjunction φ ψ).size = φ.size + ψ.size + 1

theorem Complexity.DescriptiveComplexity.isExistSO_mergeExist_internal {V : Vocabulary} (isConjunction : Bool) {rctx : List Nat} {n : Nat} (φ ψ : SOFormula V rctx n) : φ.IsExistSO → ψ.IsExistSO → (SOFormula.mergeExist isConjunction φ ψ).IsExistSO

theorem Complexity.DescriptiveComplexity.mergeExist_sat_internal {V : Vocabulary} (isConjunction : Bool) {rctx : List Nat} {n : Nat} (φ ψ : SOFormula V rctx n) (A : FinStruct V) (σ : Env A.card n) (ρ : REnv A.card rctx) : SOFormula.Sat A σ ρ (SOFormula.mergeExist isConjunction φ ψ) ↔ if isConjunction = true then SOFormula.Sat A σ ρ φ ∧ SOFormula.Sat A σ ρ ψ else SOFormula.Sat A σ ρ φ ∨ SOFormula.Sat A σ ρ ψ