Simplified definition of equality, remove `R_covered`

* I simplified the definition of equality, which shortens many proofs
by 50%.
* I removed the faulty and unproved lemma `R_covered` from `Order.v`.