simp [System.theory]
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
hp : p ∈ theory 𝐈𝐧𝐭
⊢ p ∈ theory 𝐂𝐥
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
hp : p ∈ theory 𝐈𝐧𝐭
⊢ 𝐂𝐥 ⊢! p