simp_all
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
this✝ :
  ∑ x ∈ X \ Cond ∪ Res, zlengthOf x + ∑ x ∈ X \ Cond ∩ Res, zlengthOf x =
    ∑ x ∈ X \ Cond, zlengthOf x + ∑ x ∈ Res, zlengthOf x
this : zlengthOfSet (X \ Cond ∩ Res) ≥ 0
⊢ zlengthOfSet (X \ Cond ∪ Res) ≤ zlengthOfSet (X \ Cond) + zlengthOfSet Res
X Cond Res : Finset Formula
hyp : Res.sum lengthOfFormula < Cond.sum lengthOfFormula
precondProof : Cond ⊆ X
this✝ :
  ∑ x ∈ X \ Cond ∪ Res, ↑(lengthOfFormula x) + ∑ x ∈ X \ Cond ∩ Res, ↑(lengthOfFormula x) =
    ∑ x ∈ X, ↑(lengthOfFormula x) - ∑ x ∈ Cond, ↑(lengthOfFormula x) + ∑ x ∈ Res, ↑(lengthOfFormula x)
this : 0 ≤ ∑ x ∈ X \ Cond ∩ Res, ↑(lengthOfFormula x)
⊢ ∑ x ∈ X \ Cond ∪ Res, ↑(lengthOfFormula x) ≤
    ∑ x ∈ X, ↑(lengthOfFormula x) - ∑ x ∈ Cond, ↑(lengthOfFormula x) + ∑ x ∈ Res, ↑(lengthOfFormula x)