-
Robbert Krebbers authored
Remarks: * eauto needs more fuel to automatically solve the side-conditions. * ssreflect rewrite works if we do a set (φ ..) first. No idea why.
59ae6b91
Remarks: * eauto needs more fuel to automatically solve the side-conditions. * ssreflect rewrite works if we do a set (φ ..) first. No idea why.