A simple solution for persintence could be that every level (at least the named ones), after solved, becomes a new rule you can use. Need some way of organizing so you can easily find them, though. If/when I add first order logic I think something like this would be very useful or the proofs might get very long.