proposition: Lemma refines_trans A B C (rAB : A -> B -> Type) (rBC : B -> C -> Type) (rAC : A -> C -> Type) (a : A) (b : B) (c : C) : composable rAB rBC rAC -> refines rAB a b -> refines rBC b c -> refines rAC a c.
proof: Proof. by rewrite !refinesE composableE => rABC rab rbc; apply: rABC; exists b. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq ssralg) CoqEAL(hrel param) ssrmatching