dsimp [toPropFormula]
case hNec
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hp✝ : 𝐆𝐋 ⊢ p✝
a✝ : 𝐆𝐋 ⊢! p✝ → 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
h : 𝐆𝐋 ⊢! □p✝
⊢ 𝐂𝐥 ⊢! ((□p✝)ⱽᴾ) ⋯
case hNec
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hp✝ : 𝐆𝐋 ⊢ p✝
a✝ : 𝐆𝐋 ⊢! p✝ → 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
h : 𝐆𝐋 ⊢! □p✝
⊢ 𝐂𝐥 ⊢! ⊤