Assumption handling (or lack thereof) in presence of imports

[sankalpgambhir]

Certain tactics and steps rely on external imports, but these operations will not produce sequents with assumptions. Consider for example:

// over yonder
val ab = have(A |- B) by Magic
val bc = have(B |- C) by Magic

// new running proof
assume(D)
have(A |- C) by Cut(ab, bc)
// internally this becomes:
// have({D, A} |- C) by Cut(ab, bc)
// which obviously fails :( 

This was found in the case of instantiating definitions, where a definition cannot be instantiated in the presence of assumptions as it is a weakened sequent.

Solutions:

• make all tactics allow weakened premises. This could sometimes have counterintuitive results (but I will have to work to find a good example).
• handle assumption tracking more carefully. This brings a lot of complexity to the system, and may be detrimental to predictability.

Is this a bug? Should I mark it as such? I think it is 🤔