proposition: Lemma refines_if_expr (A C : Type) (b1 b2 : bool) (vt1 vf1 : A) (vt2 vf2 : C) (R : A -> C -> Type) : refines bool_R b1 b2 -> (b1 -> b2 -> R vt1 vt2) -> (~~ b1 -> ~~ b2 -> R vf1 vf2) -> refines R (if_expr b1 vt1 vf1) (if_expr b2 vt2 vf2).
proof: Proof. move/refines_bool_eq/refinesP=> Hb; rewrite -!{}Hb => Ht Hf. rewrite /if_expr !refinesE; case: b1 Ht Hf => Ht Hf. exact: Ht. exact: Hf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq ssralg) CoqEAL(hrel param) ssrmatching