Change Details

This is not really related to the proof inventories, and more tests are coming so better split it out. There is no change in behavior.

This is not really related to the proof inventories, and more tests are coming so better split it out. There is no change in behavior. Depends on D11388.

This is not really related to the proof inventories, and more tests are coming so better split it out. There is no change in behavior. Depends on D11388.