nth_rw 1 [←(normal_has_nec (𝓓 := 𝓓))]
α : Type u_1
inst✝¹ : DecidableEq α
𝓓 𝓓₁ 𝓓₂ : DeductionParameter α
inst✝ : 𝓓.Normal
⊢ 𝓓.rules = { nec := true, loeb := false, henkin := false }
α : Type u_1
inst✝¹ : DecidableEq α
𝓓 𝓓₁ 𝓓₂ : DeductionParameter α
inst✝ : 𝓓.Normal
⊢ 𝓓.rules = { nec := 𝓓.rules.nec, loeb := false, henkin := false }