simp_all only [Multiset.mem_cons, or_true, implies_true, true_implies, forall_eq_or_imp, Multiset.add_cons]
case intro.cons
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
M0 : Multiset α
H1 : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
H2 : AccM_1 M0
H3 : ∀ (M : Multiset α), MultisetRedLt M M0 → AccM_1 (a ::ₘ M)
N : Multiset α
N_lt : MultisetRedLt N (a ::ₘ M0)
h : α
s✝ : Multiset α
a✝ : (∀ x ∈ s✝, x < a) → AccM_1 (M0 + s✝)
H0 : ∀ x ∈ h ::ₘ s✝, x < a
⊢ AccM_1 (M0 + h ::ₘ s✝)
no goals