<div dir="ltr">1. Always using extended lambda syntax (i.e. - \{ ...  -> ... }) seems to make the Emacs mode interactive goal solving assistant more capable.<div><br><div>2. `C-c C-c` works not only for case expansion, but also for single term expansion. For instance, it will expand "\{ x -> ... }" to "\{ < foo , bar > -> ...}", when appropriate (i.e. - when x is an existential or product). (Very helpful when first learning existentials.)</div><div><br></div><div>-db</div></div><div><br></div></div>