Upstreaming a small collection of lemmas

This MR upstreams a small collection of lemmas from Islaris.

Thanks for the MR.

I wonder if for Is_true_false_iff and ne_Some_eq_None it doesn't make more sense to turn the original lemmas into an . I think the lemmas are not used often, so that would prevent a further proliferation of lemmas.

Opinions?

added 1 commit

• df5b9420 - Upstreaming a small collection of lemmas

Compare with previous version

added 1 commit

• 7122b081 - Upstreaming a small collection of lemmas

Compare with previous version

added 1 commit

• eddd725b - Upstreaming a small collection of lemmas

Compare with previous version

I also added Is_true_true with _1 and _2 variants and Z_lnot_opp to this MR.

Aside from small nits, LGTM.

added 1 commit

• b692d595 - Upstreaming a small collection of lemmas

Compare with previous version

added 1 commit

• d301b744 - Upstreaming a small collection of lemmas

Compare with previous version

added 1 commit

• cb25928e - Upstreaming a small collection of lemmas

Compare with previous version

resolved all threads

mentioned in commit c2bad317

merged

@iris-users this is a breaking change:

• Rename Is_true_false → Is_true_false_2 and eq_None_ne_Some → eq_None_ne_Some_1.