constructor
case h
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
pI_prop : voc θ ⊆ jvoc X ∧ ¬satisfiable ((~θ) :: X.left) ∧ ¬satisfiable (θ :: X.right)
⊢ Interpolant φ ψ θ
case h.left
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
pI_prop : voc θ ⊆ jvoc X ∧ ¬satisfiable ((~θ) :: X.left) ∧ ¬satisfiable (θ :: X.right)
⊢ voc θ ⊆ voc φ ∩ voc ψ

case h.right
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
pI_prop : voc θ ⊆ jvoc X ∧ ¬satisfiable ((~θ) :: X.left) ∧ ¬satisfiable (θ :: X.right)
⊢ φ⊨θ ∧ θ⊨ψ