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