contradiction
case inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
neq₁ : ¬x = y
ab : x ≤ y
neq₂ : ¬y = x
ba : y ≤ x
eq : x = y
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }
no goals