fix Coq 8.18 deprecation warnings
Coq started warning about Let. ... Qed.
. And it is right, this makes little sense -- Let
means "make this completely transparent after the section"; Qed
means "make this opaque".
So let's either make these non-Qed
when the proofs are completely trivial, or non-Let
when the proofs are complicated enough that we want them to be opaque.