Skip to content

remove util/rewrite_facilities.v

Sergey Bozhko requested to merge sbozhko/rt-proofs:remove_rf into master

I think that this experiment was not successful. These lemmas can be easily replaced by ssreflect's tactics. Also, they encourage to write proofs that are harder to maintain.

Merge request reports