no goals
α : Type u
β : Type v
l l₁ l₂ : List α
r✝ : α → α → Prop
a b : α
r : α → β → Prop
hr : Relator.BiUnique r
⊢ (fun x x_1 => x ↔ x_1) (Nodup []) (Nodup [])
simp only [nodup_nil]
no goals
α : Type u
β : Type v
l l₁ l₂ : List α
r✝ : α → α → Prop
a b : α
r : α → β → Prop
hr : Relator.BiUnique r
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
hab : r a✝ b✝
h : Forall₂ r l₁✝ l₂✝
⊢ (fun x x_1 => x ↔ x_1) (Nodup (a✝ :: l₁✝)) (Nodup (b✝ :: l₂✝))
simpa only [nodup_cons] using
  Relator.rel_and (Relator.rel_not (rel_mem hr hab h)) (rel_nodup hr h)