Theorem: LO.Modal.Standard.DeductionParameter.normal_rules (Logic/Modal/Standard/Deduction.lean)

State before:
α : Type u_1
inst✝² : DecidableEq α
𝓓 𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
⊢ 𝓓₁.rules = 𝓓₂.rules
Tactic:
simp
State after:
no goals