Port syntax for internalCmraValid, internalEq, internalIncluded

[MackieLoeffel]

Summary

Port the syntax of internalCmraValid, internalEq and internalIncluded in bi/cmra.v and bi/internal_eq.v.

Subtasks

• internalCmraValid
• internalEq
• internalIncluded

Dependencies

Rocq dependencies:

• Port bi/internal_eq.v #250
• Port bi/cmra.v #278

[MackieLoeffel]

@markusdemedeiros Was there a technical reason why you did not port the notations during #178 or did you just not get around to it?

[markusdemedeiros]

Didn't get around to it