finish inversion lemmas. trustmes are gone, proof ok