proposition: Lemma coqeal_eq C {eqC : strategy_class C} {T T'} spec (x x' : T) {y y' : T'} {rxy : refines eq (spec_id x) (spec y)} {ry : C _ y y'} {rx : simpl (spec y') x'} : x = x'.
proof: Proof. by rewrite eqC in ry; rewrite -rx -ry; apply: refines_eq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq ssralg) CoqEAL(hrel param) ssrmatching