case cons
α : Type u
r : α → α → Prop
inst✝ : IsIrrefl α r
a : α
l₁ l₂ : List α
h : Lex r l₁ l₂
⊢ Lex r l₁ l₂

case rel
α : Type u
r : α → α → Prop
inst✝ : IsIrrefl α r
a : α
l₁ l₂ : List α
h : r a a
⊢ Lex r l₁ l₂
α : Type u
r : α → α → Prop
inst✝ : IsIrrefl α r
a : α
l₁ l₂ : List α
h : Lex r (a :: l₁) (a :: l₂)
⊢ Lex r l₁ l₂
cases' h with _ _ _ _ _ h _ _ _ _ h
no goals
case cons
α : Type u
r : α → α → Prop
inst✝ : IsIrrefl α r
a : α
l₁ l₂ : List α
h : Lex r l₁ l₂
⊢ Lex r l₁ l₂

case rel
α : Type u
r : α → α → Prop
inst✝ : IsIrrefl α r
a : α
l₁ l₂ : List α
h : r a a
⊢ Lex r l₁ l₂
exacts [h, (irrefl_of r a h).elim]