• Robbert Krebbers's avatar
    Avoid use of `solve_proper`. · c579b46c
    Robbert Krebbers authored
    Due to Coq bug #10480 or #10474 it actually used `Morphisms.solve_proper`
    instead of the version of std++. The version in std++ can inherently
    not solve this, so I changed it into a manual proof.
    c579b46c