exact h
case h_2.inr.h_2.inr.refl.refl.refl.refl
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p₁ : succ (List.length xs) = m
y : ℕ
ys : List ℕ
p₂ : succ (List.length ys) = m
z : ℕ
zs : List ℕ
p₃ : succ (List.length zs) = m
v₁✝¹ v₂✝¹ v₁✝ v₂✝ : Vector ℕ m
property✝³ : succ (List.length xs) = m
eq : ¬x = y
h : x ≤ y
property✝² : succ (List.length ys) = m
property✝¹ : succ (min (List.length xs) (List.length zs)) = m
h✝ : ¬x = y
property✝ : succ (min (List.length ys) (List.length zs)) = m
⊢ x ≤ y
no goals