intro h
α : Type u_1
inst✝ : DecidableEq α
p✝ : Formula α
m𝓓 : DeductionParameter α
p : Superintuitionistic.Formula α
⊢ 𝐂𝐥 ⊢! p → m𝓓 ⊢! pᴹ
α : Type u_1
inst✝ : DecidableEq α
p✝ : Formula α
m𝓓 : DeductionParameter α
p : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! p
⊢ m𝓓 ⊢! pᴹ