Creating a subst-able definition

Stream: new members

[Robert Maxton]

How do you save an some intermediate result in such a way as to be able to access it later? let doesn't work with subst as far as I can tell. So far, the best I can come up with is a pattern have: ∃ x, p x, cases have with x xdef, but that 's a really wordy workaround...

[Robert Maxton]

aaaand not a minute later I discover set. Nevermind, I guess?