simp
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
property✝¹ property✝ : List.length [] = m
h : algebra.Order.ble_lex_impl { val := [], property := property✝¹ } { val := [], property := property✝ } = true
⊢ match { val := [], property := property✝¹ }, { val := [], property := property✝ } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y :: tail_1, property := property_1 } =>
    if x = y then
      lex_impl (Vector.tail { val := [], property := property✝¹ }) (Vector.tail { val := [], property := property✝ })
    else x ≤ y
no goals