Skip to content

Add instance `cons_equiv_inj`.

Robbert Krebbers requested to merge robbert/cons_equiv_inj into master

Similar to iris!995 (merged)

Also took the liberty to name the one for eq.

Merge request reports