rcases isVar with ⟨v1, _, rfl⟩
case a.mp
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v2 : ν₂
h : v2 ∈ PropFun.semVars ⟦map f φ⟧
isVar : ∃ a ∈ vars φ, f a = v2
⊢ ∃ a ∈ PropFun.semVars ⟦φ⟧, f a = v2
case a.mp.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
left✝ : v1 ∈ vars φ
h : f v1 ∈ PropFun.semVars ⟦map f φ⟧
⊢ ∃ a ∈ PropFun.semVars ⟦φ⟧, f a = f v1