Case should add expl to its new subgoals
The transformation "case" should add explanation labels to its subgoals (because these labels are visible in the proof tree). This is more clear for the user.
Transformations induction and others could also take benefits from this.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information