justification done
justification done
The user is proving a sequent which was opened with the tactic we need to prove, or the user is proving a sequent which was opened with the tactic we proceed by induction/cases on, or the user is proving a chain of equalities that was started with either the tactic conclude or obtain.
It closes the current sequent with the given justification.
None.