exact h
case mk
α : Type u_1
inst✝ : DecidableEq α
𝓓 𝓓₁ : DeductionParameter α
axiomSet✝ : AxiomSet α
rules✝ : DeductionParameterRules
h : 𝓓₁.rules = { axiomSet := axiomSet✝, rules := rules✝ }.rules
⊢ ((𝓓₁ ⊔ { axiomSet := axiomSet✝, rules := rules✝ }) h).rules = { axiomSet := axiomSet✝, rules := rules✝ }.rules
no goals