move lemma from sholSemantics into modelSet