adding a stub theorem for what complete progress probably looks like.
adding a stub theorem for what complete progress probably looks like.

@cyrus- i'm not quite sure what complete preservation looks like. the
statement of preservation is actually pretty standard, so i don't know what
the adjustment would be. maybe that you just don't add any casts or
something? there are no casts in hexps so a complete term won't have any;
if we believe that casts are a thing that results from holes being
indeterminate, we shouldn't add any. that's probably a theorem we should be
proving but i'm not sure it's preservation.

hazelgrove/hazelnut-dynamics-agda