In addition to #12, we could add labeled assumptions: ``` @firstprem a and b: premise @box1 |[ ~b: assumption b: and elim2 1 _|_ ]| b: PBC @box1 ```
