@[simp]

theorem union_singleton_is_insert {X : Finset Formula} {ϕ : Formula} : X ∪ {ϕ} = insert ϕ X

@[simp]

theorem sdiff_singleton_is_erase {X : Finset Formula} {ϕ : Formula} : X \ {ϕ} = X.erase ϕ

@[simp]

theorem lengthAdd {X : Finset Formula} {ϕ : Formula} : ϕ ∉ X → lengthOfSet (insert ϕ X) = lengthOfSet X + lengthOfFormula ϕ

@[simp]

theorem lengthOf_insert_leq_plus {X : Finset Formula} {ϕ : Formula} : lengthOfSet (insert ϕ X) ≤ lengthOfSet X + lengthOfFormula ϕ

@[simp]

theorem lengthRemove (X : Finset Formula) (ϕ : Formula) : ϕ ∈ X → lengthOfSet (X.erase ϕ) + lengthOfFormula ϕ = lengthOfSet X

theorem lengthSetRemove (X Y : Finset Formula) (h : Y ⊆ X) : lengthOfSet (X \ Y) + lengthOfSet Y = lengthOfSet X

theorem lengthOfEqualSets (X Y : Finset Formula) : X = Y → lengthOfSet X = lengthOfSet Y

@[simp]

theorem sum_union_le {T : Type u_1} [DecidableEq T] {X Y : Finset T} {F : T → ℕ} : (X ∪ Y).sum F ≤ X.sum F + Y.sum F