constructor
case a
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOf (insert ϕ (X \ {ϕ})) = lengthOf (X \ {ϕ}) + lengthOfFormula ϕ
a✝ : Formula
⊢ a✝ = ϕ ∨ a✝ ∈ X ∧ ¬a✝ = ϕ ↔ a✝ ∈ X
case a.mp
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOf (insert ϕ (X \ {ϕ})) = lengthOf (X \ {ϕ}) + lengthOfFormula ϕ
a✝ : Formula
⊢ a✝ = ϕ ∨ a✝ ∈ X ∧ ¬a✝ = ϕ → a✝ ∈ X

case a.mpr
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOf (insert ϕ (X \ {ϕ})) = lengthOf (X \ {ϕ}) + lengthOfFormula ϕ
a✝ : Formula
⊢ a✝ ∈ X → a✝ = ϕ ∨ a✝ ∈ X ∧ ¬a✝ = ϕ