case mk.mk
M : Type u_1
N : Type ?u.6337
P : Type ?u.6340
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c d : Con M
r✝ : M → M → Prop
iseqv✝ : Equivalence r✝
mul'✝ : ∀ {w x y z : M}, r w x → r y z → r (w * y) (x * z)
H : r = r
⊢ { toSetoid := { r := r✝, iseqv := iseqv✝ }, mul' := mul'✝ } = d
M : Type u_1
N : Type ?u.6337
P : Type ?u.6340
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ c d : Con M
H : r = r
⊢ c = d
rcases c with ⟨⟨⟩⟩
case mk.mk.mk.mk
M : Type u_1
N : Type ?u.6337
P : Type ?u.6340
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r✝¹ : M → M → Prop
iseqv✝¹ : Equivalence r✝¹
mul'✝¹ : ∀ {w x y z : M}, r w x → r y z → r (w * y) (x * z)
r✝ : M → M → Prop
iseqv✝ : Equivalence r✝
mul'✝ : ∀ {w x y z : M}, r w x → r y z → r (w * y) (x * z)
H : r = r
⊢ { toSetoid := { r := r✝¹, iseqv := iseqv✝¹ }, mul' := mul'✝¹ } =
    { toSetoid := { r := r✝, iseqv := iseqv✝ }, mul' := mul'✝ }
case mk.mk
M : Type u_1
N : Type ?u.6337
P : Type ?u.6340
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c d : Con M
r✝ : M → M → Prop
iseqv✝ : Equivalence r✝
mul'✝ : ∀ {w x y z : M}, r w x → r y z → r (w * y) (x * z)
H : r = r
⊢ { toSetoid := { r := r✝, iseqv := iseqv✝ }, mul' := mul'✝ } = d
rcases d with ⟨⟨⟩⟩
case mk.mk.mk.mk.refl
M : Type u_1
N : Type ?u.6337
P : Type ?u.6340
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r✝ : M → M → Prop
iseqv✝¹ : Equivalence r✝
mul'✝¹ : ∀ {w x y z : M}, r w x → r y z → r (w * y) (x * z)
iseqv✝ : Equivalence r✝
mul'✝ : ∀ {w x y z : M}, r w x → r y z → r (w * y) (x * z)
⊢ { toSetoid := { r := r✝, iseqv := iseqv✝¹ }, mul' := mul'✝¹ } =
    { toSetoid := { r := r✝, iseqv := iseqv✝ }, mul' := mul'✝ }
case mk.mk.mk.mk
M : Type u_1
N : Type ?u.6337
P : Type ?u.6340
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r✝¹ : M → M → Prop
iseqv✝¹ : Equivalence r✝¹
mul'✝¹ : ∀ {w x y z : M}, r w x → r y z → r (w * y) (x * z)
r✝ : M → M → Prop
iseqv✝ : Equivalence r✝
mul'✝ : ∀ {w x y z : M}, r w x → r y z → r (w * y) (x * z)
H : r = r
⊢ { toSetoid := { r := r✝¹, iseqv := iseqv✝¹ }, mul' := mul'✝¹ } =
    { toSetoid := { r := r✝, iseqv := iseqv✝ }, mul' := mul'✝ }
cases H
no goals
case mk.mk.mk.mk.refl
M : Type u_1
N : Type ?u.6337
P : Type ?u.6340
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r✝ : M → M → Prop
iseqv✝¹ : Equivalence r✝
mul'✝¹ : ∀ {w x y z : M}, r w x → r y z → r (w * y) (x * z)
iseqv✝ : Equivalence r✝
mul'✝ : ∀ {w x y z : M}, r w x → r y z → r (w * y) (x * z)
⊢ { toSetoid := { r := r✝, iseqv := iseqv✝¹ }, mul' := mul'✝¹ } =
    { toSetoid := { r := r✝, iseqv := iseqv✝ }, mul' := mul'✝ }
congr