have ctX : ClosedTableau ([],[]) X :=
  by
  rw [tautImp_iff_TNodeUnsat rfl] at hyp
  rw [← completeness] at hyp simp [consistent,inconsistent] at hyp
  exact Classical.choice hyp
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
⊢ ∃ θ, Interpolant φ ψ θ
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
⊢ ∃ θ, Interpolant φ ψ θ