I’d be in favour! Larry > On 23 Feb 2019, at 15:07, Makarius <makarius at sketis.net> wrote: > > It might be better to introduce a proof-local version of 'abbreviation'.