More fixes to Lemma 1 of the proof and misc. subroutines