split out HLevelsBase; prove Is_true_hprop

[andres-erbsen]

This change was discussed extensively at rocq-prover/rocq#19747 with no remaining objections.

• Added changelog.
• Updated test suite

[andres-erbsen]

The CI errors look unrelated to me, but I'd appreciate another pair of eyes that.

jasmin:

[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]File "./itrees/xrutt.v", line 26, characters 5-21:
Error: Cannot find a physical path bound to logical path
Structures.Monad with prefix ExtLib.

elpi:

warning: error: unable to download 'https://github.com/LPCIC/coq-elpi/archive/master.tar.gz': HTTP error 500

metacoq-utils:

sed: can't read ./template-coq/gen-src/to-lower.sh: No such file or directory

[andres-erbsen]

@vbgl: Can you advise whether the CI failure for Jasmin indicates a problem with this PR? Thanks!
@mattam82: Can you advise whether the CI failure for Metarocq indicates a problem with this PR? Thanks!

[vbgl]

Regarding the Jasmin failure, this is probably a bug in the CI infrastructure (undeclared dependency) so unrelated to this PR.

[mattam82]

I think the CI failure on metarocq indicates that we must update the nix derivation in the stdlib CI

[andres-erbsen]

Thank you! I intend to merge after I put changelog in the right place, perhaps tomorrow.