intro d
case mp
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
⊢ 𝐈𝐧𝐭 ⊢! ~p → 𝐂𝐥 ⊢! ~p
case mp
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
d : 𝐈𝐧𝐭 ⊢! ~p
⊢ 𝐂𝐥 ⊢! ~p