lebedev.ri added a comment. Here's what i wanted to see: https://alive2.llvm.org/ce/z/2XpHkB Did i mess that proof up, or are some new preconditions needed? CHANGES SINCE LAST ACTION https://reviews.llvm.org/D108049/new/ https://reviews.llvm.org/D108049