Currently, destruct only destruct the logic connector (/, /, =>) at the head of a formula. It could recursively be called on the generated new hypotheses.
This should be implemented as a new name or boolean parameter.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information