simp [voc,jvoc,vocabOfListFormula,vocabOfFormula] at pI_prop
case h.left
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
pI_prop : voc θ ⊆ jvoc X ∧ ¬satisfiable ((~θ) :: X.left) ∧ ¬satisfiable (θ :: X.right)
f : ℕ
f_in : f ∈ voc θ
⊢ f ∈ voc φ ∩ voc ψ
case h.left
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
f : ℕ
f_in : f ∈ voc θ
pI_prop :
  vocabOfFormula θ ⊆ vocabOfFormula φ ∩ vocabOfFormula ψ ∧
    (∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x), ¬evaluate x_1 x_2 θ → ¬evaluate x_1 x_2 φ) ∧
      ∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x), evaluate x_1 x_2 θ → evaluate x_1 x_2 ψ
⊢ f ∈ voc φ ∩ voc ψ