move theory about constrained extensions here

also, add constrainable_update and prove that type definitions are such.