A well-known (in narrow circles) take lemma for finite lists via the generalized take_take:
Lemma take_take_min {T} i j (s : seq T) : take i (take j s) = take (minn i j) s.
Proof. by elim: s i j => //= a l IH [|i] [|j] //=; rewrite minnSS IH. Qed.
Lemma take_lemma {T} (p r : seq T) : (forall i, take i p = take i r) <-> p = r.
Proof.
split; last by move=>->.
move=>H; move: (H (size p)) (H (size r)); rewrite !take_size=>{H} Hp Hr.
by rewrite Hp -Hr {2 3}Hp !take_take_min minnAC minnn minnC.
Qed.