proposition: Lemma refinesP T T' (R : T -> T' -> Type) (x : T) (y : T') : refines R x y -> R x y.
proof: Proof. by rewrite refinesE. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq ssralg) CoqEAL(hrel param) ssrmatching