Added contextual equivalence
and some structural comments