have partInt := tabToInt ctX
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
⊢ ∃ θ, Interpolant φ ψ θ
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
partInt : PartInterpolant X
⊢ ∃ θ, Interpolant φ ψ θ