Checks that expression e
is definitional equal to inst
.
Uses instances
transparency so that reducible terms and instances extended
other instances are unfolded.
Checks that expression e
is definitional equal to inst
.
Uses instances
transparency so that reducible terms and instances extended
other instances are unfolded.