. intro d; exact glivenko.mp $ dni'! d;
case mp
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
⊢ 𝐈𝐧𝐭 ⊢! ~p → 𝐂𝐥 ⊢! ~p

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