simp
case h_1
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
p q l : List.length [] = m
ab : Order.lex_impl { val := [], property := p } { val := [], property := q }
bc : Order.lex_impl { val := [], property := q } { val := [], property := l }
v₁✝ v₂✝ : Vector ℕ m
property✝¹ property✝ : List.length [] = m
heq✝¹ : { val := [], property := p } = { val := [], property := property✝¹ }
heq✝ : { val := [], property := l } = { val := [], property := property✝ }
⊢ True

case h_2
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
p q l : List.length [] = m
ab : Order.lex_impl { val := [], property := p } { val := [], property := q }
bc : Order.lex_impl { val := [], property := q } { val := [], property := l }
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := [], property := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := [], property := l } = { val := y✝ :: tail✝, property := property✝ }
⊢ if x✝ = y✝ then Order.lex_impl (tail { val := [], property := p }) (tail { val := [], property := l }) else x✝ ≤ y✝
case h_2
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
p q l : List.length [] = m
ab : Order.lex_impl { val := [], property := p } { val := [], property := q }
bc : Order.lex_impl { val := [], property := q } { val := [], property := l }
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := [], property := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := [], property := l } = { val := y✝ :: tail✝, property := property✝ }
⊢ if x✝ = y✝ then Order.lex_impl (tail { val := [], property := p }) (tail { val := [], property := l }) else x✝ ≤ y✝