have d₂ : 𝐕𝐞𝐫 ⊢! pⱽ := by simpa using of_classical h;
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐂𝐥 ⊢! (pⱽᴾ) ⋯
d₁ : 𝐕𝐞𝐫 ⊢! pⱽ ⟶ p
⊢ 𝐕𝐞𝐫 ⊢! p
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐂𝐥 ⊢! (pⱽᴾ) ⋯
d₁ : 𝐕𝐞𝐫 ⊢! pⱽ ⟶ p
d₂ : 𝐕𝐞𝐫 ⊢! pⱽ
⊢ 𝐕𝐞𝐫 ⊢! p