no goals
α : Type u
β : Type v
R r : α → α → Prop
l l₁✝ l₂✝ : List α
a b : α
l₁ l₂ l₃ : List α
h₁ : Chain' R (l₁ ++ l₂)
h₂ : Chain' R (l₂ ++ l₃)
hn : l₂ ≠ []
⊢ ∀ (x : α), x ∈ getLast? (l₁ ++ l₂) → ∀ (y : α), y ∈ head? l₃ → R x y
simpa only [getLast?_append_of_ne_nil _ hn] using (chain'_append.1 h₂).2.2