add better lemmas for working with mask-changing fupd, and rearrange names a bit See merge request !637