split
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
⊢ (match { val := y :: ys, property := q }, { val := x :: xs, property := p } with
    | { val := [], property := property }, { val := [], property := property_1 } => True
    | { val := x_1 :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
      if x_1 = y_1 then
        Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := x :: xs, property := p })
      else x_1 ≤ y_1) ∨
    if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
    else x ≤ y
case h_1
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
property✝¹ property✝ : List.length [] = m
heq✝¹ : { val := y :: ys, property := q } = { val := [], property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := [], property := property✝ }
⊢ True ∨
    if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
    else x ≤ y

case h_2
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
⊢ (if x✝ = y✝ then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
    else x✝ ≤ y✝) ∨
    if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
    else x ≤ y