proposition: Lemma refines_abstr2 A B A' B' A'' B'' (R : A -> B -> Type) (R' : A' -> B' -> Type) (R'' : A'' -> B'' -> Type) (f : A -> A' -> A'' ) (g : B -> B' -> B''): (forall (a : A) (b : B), refines R a b -> forall (a' : A') (b' : B'), refines R' a' b' -> refines R'' (f a a') (g b b')) -> refines (R ==> R' ==> R'') f g.
proof: Proof. by move=> H; do 2![eapply refines_abstr => *]; apply: H. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq ssralg) CoqEAL(hrel param) ssrmatching