α✝ : Sort ?u.8
β : Sort ?u.11
α : Sort u_1
r : α → α → Prop
iseqv✝¹ : Equivalence r
p : α → α → Prop
iseqv✝ : Equivalence p
Eq : ∀ (a b : α), Setoid.r a b ↔ Setoid.r a b
this : r = p
⊢ { r := r, iseqv := iseqv✝¹ } = { r := p, iseqv := iseqv✝ }
α✝ : Sort ?u.8
β : Sort ?u.11
α : Sort u_1
r : α → α → Prop
iseqv✝¹ : Equivalence r
p : α → α → Prop
iseqv✝ : Equivalence p
Eq : ∀ (a b : α), Setoid.r a b ↔ Setoid.r a b
⊢ { r := r, iseqv := iseqv✝¹ } = { r := p, iseqv := iseqv✝ }
have : r = p := funext fun a ↦ funext fun b ↦ propext <| Eq a b
α✝ : Sort ?u.8
β : Sort ?u.11
α : Sort u_1
r : α → α → Prop
iseqv✝¹ iseqv✝ : Equivalence r
Eq : ∀ (a b : α), Setoid.r a b ↔ Setoid.r a b
⊢ { r := r, iseqv := iseqv✝¹ } = { r := r, iseqv := iseqv✝ }
α✝ : Sort ?u.8
β : Sort ?u.11
α : Sort u_1
r : α → α → Prop
iseqv✝¹ : Equivalence r
p : α → α → Prop
iseqv✝ : Equivalence p
Eq : ∀ (a b : α), Setoid.r a b ↔ Setoid.r a b
this : r = p
⊢ { r := r, iseqv := iseqv✝¹ } = { r := p, iseqv := iseqv✝ }
subst this
no goals
α✝ : Sort ?u.8
β : Sort ?u.11
α : Sort u_1
r : α → α → Prop
iseqv✝¹ iseqv✝ : Equivalence r
Eq : ∀ (a b : α), Setoid.r a b ↔ Setoid.r a b
⊢ { r := r, iseqv := iseqv✝¹ } = { r := r, iseqv := iseqv✝ }
rfl