case nil
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
h : ∀ (a : α), ¬[a, a] <+ []
⊢ Nodup []

case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a✝ b a : α
l : List α
IH : (∀ (a : α), ¬[a, a] <+ l) → Nodup l
h : ∀ (a_1 : α), ¬[a_1, a_1] <+ a :: l
⊢ Nodup (a :: l)
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
⊢ (∀ (a : α), ¬[a, a] <+ l) → Nodup l
induction' l with a l IH <;> intro h
no goals
case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a✝ b a : α
l : List α
IH : (∀ (a : α), ¬[a, a] <+ l) → Nodup l
h : ∀ (a_1 : α), ¬[a_1, a_1] <+ a :: l
⊢ Nodup (a :: l)
exact (IH fun a s => h a <| sublist_cons_of_sublist _ s).cons fun al =>
  h a <| (singleton_sublist.2 al).cons_cons _
no goals
case nil
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
h : ∀ (a : α), ¬[a, a] <+ []
⊢ Nodup []
exact nodup_nil