proposition: Lemma refines_abstr A B C D (R : A -> B -> Type) (R' : C -> D -> Type) (c : A -> C) (d : B -> D): (forall (a : A) (b : B), refines R a b -> refines R' (c a) (d b)) -> refines (R ==> R') c d.
proof: Proof. by rewrite !refinesE; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq ssralg) CoqEAL(hrel param) ssrmatching