done with extend lemmas, only one trustme left: stp-trans