∀ {α : Type u_1} [inst : BEq α] (x x_1 : List α),
  x.dropPrefix? x_1 =
    match x, x_1 with
    | list, [] => some list
    | [], head :: tail => none
    | a :: as, b :: bs => if (a == b) = true then as.dropPrefix? bs else none