Verification rules for program lowering

Import this module explicitly when proving that an einsum plan preserves semantics. The rules compare an already checked plan with its tensor semantics. They do not certify the parser, native compilation, or an external kernel; those require separate evidence.