constructor
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐕𝐞𝐫 ⊢! p ↔ 𝐂𝐥 ⊢! (pⱽᴾ) ⋯
case mp
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐕𝐞𝐫 ⊢! p → 𝐂𝐥 ⊢! (pⱽᴾ) ⋯

case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐂𝐥 ⊢! (pⱽᴾ) ⋯ → 𝐕𝐞𝐫 ⊢! p