WIP: rlwinm/rlwnm/rlwimi-type proofs