Alternative take on making proof mode terms more compact.
This is an alternative to !224 (closed) by splitting up envs_lookup_delete
premises into envs_lookup
and envs_delete
.
@jtassaro Could you rebase !224 (closed) so we can compare?
The following tactics involve some other tricks:
-
tac_assumption
: uses a let binding forenvs_delete
since its result is used twice -
tac_specialize
: uses a let binding forenvs_delete
since its result is used twice -
tac_specialize_assert
: uses a conjunction, not sure if it's worth the extra bloat in the Ltac code to do something smarter here.