simp [map₂, Variables.mul, List.zipWith] at var_mul₁ var_mul₂
case h_2.inr.h_2.inr.refl.refl
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p₁ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
p₂ : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
p₃ : List.length (z :: zs) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝³ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝² : List.length (y✝ :: tail✝) = m
var_mul₁ :
  Variables.mul { val := x :: xs, property := p₁ } { val := z :: zs, property := p₃ } =
    { val := x✝ :: tail✝¹, property := property✝³ }
var_mul₂ :
  Variables.mul { val := y :: ys, property := p₂ } { val := z :: zs, property := p₃ } =
    { val := y✝ :: tail✝, property := property✝² }
h✝ : ¬x✝ = y✝
v₁✝ v₂✝ : Vector ℕ m
property✝¹ : List.length (x :: xs) = m
eq : ¬x = y
h : x ≤ y
property✝ : List.length (y :: ys) = m
⊢ x✝ ≤ y✝
case h_2.inr.h_2.inr.refl.refl
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p₁ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
p₂ : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
p₃ : List.length (z :: zs) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝³ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝² : List.length (y✝ :: tail✝) = m
var_mul₁ :
  { val := (x + z) :: List.zipWith (fun x y => x + y) xs zs,
      property := (_ : (fun l => List.length l = m) ((x + z) :: List.zipWith (fun x y => x + y) xs zs)) } =
    { val := x✝ :: tail✝¹, property := property✝³ }
var_mul₂ :
  { val := (y + z) :: List.zipWith (fun x y => x + y) ys zs,
      property := (_ : (fun l => List.length l = m) ((y + z) :: List.zipWith (fun x y => x + y) ys zs)) } =
    { val := y✝ :: tail✝, property := property✝² }
h✝ : ¬x✝ = y✝
v₁✝ v₂✝ : Vector ℕ m
property✝¹ : List.length (x :: xs) = m
eq : ¬x = y
h : x ≤ y
property✝ : List.length (y :: ys) = m
⊢ x✝ ≤ y✝