proposition: Lemma refines_comp_unify A B (R : A -> B -> Type) x y : refines (R \o (@unify B))%rel x y -> refines R x y.
proof: Proof. move=> /refines_split12. rewrite !refinesE=> H. case: H=> ? h. case: h=> ? h2. by rewrite -h2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq ssralg) CoqEAL(hrel param) ssrmatching