dsimp [VerTranslation, toPropFormula] at ih₁ ih₂
case mp.hMdp
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h₁ : 𝐕𝐞𝐫 ⊢ p✝ ⟶ q✝
h₂ : 𝐕𝐞𝐫 ⊢ p✝
ih₁ : 𝐕𝐞𝐫 ⊢! p✝ ⟶ q✝ → 𝐂𝐥 ⊢! ((p✝ ⟶ q✝)ⱽᴾ) ⋯
ih₂ : 𝐕𝐞𝐫 ⊢! p✝ → 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
h : 𝐕𝐞𝐫 ⊢! q✝
⊢ 𝐂𝐥 ⊢! (q✝ⱽᴾ) ⋯
case mp.hMdp
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h₁ : 𝐕𝐞𝐫 ⊢ p✝ ⟶ q✝
h₂ : 𝐕𝐞𝐫 ⊢ p✝
ih₁ : 𝐕𝐞𝐫 ⊢! p✝ ⟶ q✝ → 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯ ⟶ (q✝ⱽᴾ) ⋯
ih₂ : 𝐕𝐞𝐫 ⊢! p✝ → 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
h : 𝐕𝐞𝐫 ⊢! q✝
⊢ 𝐂𝐥 ⊢! (q✝ⱽᴾ) ⋯