constructor
case right.intro
α : Type
inst✝ : Inhabited α
p : Formula α
hp : 𝐈𝐧𝐭 ⊬! p ⋎ ~p
⊢ 𝐂𝐥 ⊢! p ⋎ ~p ∧ ¬𝐈𝐧𝐭 ⊢! p ⋎ ~p
case right.intro.left
α : Type
inst✝ : Inhabited α
p : Formula α
hp : 𝐈𝐧𝐭 ⊬! p ⋎ ~p
⊢ 𝐂𝐥 ⊢! p ⋎ ~p

case right.intro.right
α : Type
inst✝ : Inhabited α
p : Formula α
hp : 𝐈𝐧𝐭 ⊬! p ⋎ ~p
⊢ ¬𝐈𝐧𝐭 ⊢! p ⋎ ~p