rw [hl.eq_take]
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
hl : l <+: l'
h : l.length ≤ n
⊢ l <+: take n l'
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
hl : l <+: l'
h : l.length ≤ n
⊢ take l.length l' <+: take n l'