simp
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
p q : List.length [] = m
ab : Order.lex_impl { val := [], property := p } { val := [], property := q }
ba : Order.lex_impl { val := [], property := q } { val := [], property := p }
⊢ { val := [], property := p } = { val := [], property := q }
no goals