feat: ensure nested proofs having been abstracted in equation and unfold auxiliary theorems
6 files changed