Sometimes underscores in lemma prevents proofs 