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

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

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

State before:
α : Type u_1
inst✝¹ : DecidableEq α
𝓓 𝓓₁ 𝓓₂ : DeductionParameter α
inst✝ : 𝓓.Normal
⊢ 𝓓.rules = { nec := 𝓓.rules.nec, loeb := 𝓓.rules.loeb, henkin := false }
Tactic:
nth_rw 1 [←(notmal_not_has_henkin (𝓓 := 𝓓))]
State after:
no goals