more fixes to lemmas
substitution lemma
defined a bunch of equivalence relations for compatibility lemmas