have H3:= take_append_drop a.length (a ++ b)
α : Type u_1
a b : List α
⊢ take a.length (a ++ b) = a
α : Type u_1
a b : List α
H3 : take a.length (a ++ b) ++ drop a.length (a ++ b) = a ++ b
⊢ take a.length (a ++ b) = a