. intro h;
  have d₁ : 𝐕𝐞𝐫 ⊢! pⱽ ⟶ p := conj₂'! deducible_iff_verTranslation;
  have d₂ : 𝐕𝐞𝐫 ⊢! pⱽ := by simpa using of_classical h;
  exact d₁ ⨀ d₂;
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐂𝐥 ⊢! (pⱽᴾ) ⋯ → 𝐕𝐞𝐫 ⊢! p
no goals