add lemma
modify definition of ctxleq