no goals
α : Type u_1
β : Type ?u.483
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
⊢ a :: l ∈ subchain s ↔ a ∈ s ∧ l ∈ subchain s ∧ ∀ (b : α), b ∈ head? l → a < b
simp only [subchain, mem_setOf_eq, forall_mem_cons, chain'_cons', and_left_comm, and_comm,
  and_assoc]