reproving, up to start of semantics_simple_inst

this is the first one that looks to require some effort to update