proving quot.mk equality

Stream: general

[Bernd Losert]

How does you usually prove an equality like quot.mk r x = quot.mk r y. I see there is a theorem quot.eq, so I guess I need to produce a value of type eqv_gen r x y?

[Anne Baanen]

That would be the most general way to do it: eqv_gen r means "the equivalence relation generated by r, so it also works if r is not an equivalence relation. If it is an equivalence relation, then you can use docs#quotient.sound (or docs#quotient.sound' if the instance parameters annoy you)

[Bernd Losert]

Cool. Thanks.