class LO.Propositional.Kripke2.Model.IsHereditary (M : Model) : Prop

• hereditary {a : ℕ} {x y : M.World} : M.Val x a → x ≺ y → M.Val y a

@[simp]

theorem LO.Propositional.Kripke2.valid_axiomHrd_of_isHereditary {M : Model} {a : ℕ} [M.IsHereditary] : M ⊧ Axioms.Hrd #a

theorem LO.Propositional.Kripke2.isHereditary_of_valid_axiomHrd {M : Model} (h : ∀ (a : ℕ), M ⊧ Axioms.Hrd #a) : M.IsHereditary