Add `hoare_from_abs` rule

[michaelmcinerney]

[michaelmcinerney]

I didn't put much thought into the names of the new lemmas. Maybe valid_cross or hoare_cross might be slightly better than hoare_from_abs. But I imagine that someone would have to search for a theorem with valid and corres_underlying to find it, anyway. These lemmas are visible in AInvs, Refine, and CRefine, at least

[Xaphiosis]

I'm fine with the names. Small comments, but nothing semantic.

[michaelmcinerney]

I have responded to the comments, and also added a type signature for ex_abs_underlying

[lsf37]

This looks ready to merge now. @michaelmcinerney can you please squash that one commit?

[michaelmcinerney]

I tried to squash that one commit, but I'm not sure what's happened, with all the other merge stuff

[lsf37]

hm, yes, that looks not good :-) Let me check.

[lsf37]

Ok, I think I fixed it. (Basically started a new branch from master, cherry-picked your two commits and squashed them)

[michaelmcinerney]

Thanks!