no goals
ds₁ ds₂ ds₃ is : List ℕ
h : Forall₂ (fun x x_1 => x < x_1) is (ds₁ ++ ds₂ ++ ds₃)
⊢ ↑(take (drop (assocRight { val := is, property := h }))) = ↑(drop (take { val := is, property := h }))
simp [assocRight, take, drop, cast_type, List.drop_take]