added Require Export RelationClasses to access Reflexive class
had to change the name of hypothesis in rewrite. Probably the naming engine of 8.4 generates different names automatically for intros