. obtain ⟨_, e⟩ := hVer; subst_vars; dsimp [Axioms.Ver, VerTranslation, toPropFormula]; apply imp_id!;
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐆𝐋 ⊢! p✝
hVer : p✝ ∈ 𝗟
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
no goals