recursive destruct
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.
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.