dsimp [TrivTranslation, toPropFormula]
case mp.hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐂𝐥 ⊢! ((~~p✝ ⟶ p✝)ᵀᴾ) ⋯
case mp.hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐂𝐥 ⊢! (((p✝ᵀᴾ) ⋯ ⟶ ⊥) ⟶ ⊥) ⟶ (p✝ᵀᴾ) ⋯