dsimp [VerTranslation, toPropFormula]
case hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐆𝐋 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐂𝐥 ⊢! ((~~p✝ ⟶ p✝)ⱽᴾ) ⋯
case hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐆𝐋 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐂𝐥 ⊢! (((p✝ⱽᴾ) ⋯ ⟶ ⊥) ⟶ ⊥) ⟶ (p✝ⱽᴾ) ⋯