proposition: Lemma refineEquiv_Pick_if {A B} (P : A -> B -> Prop) : forall (cond : bool) (ta ea : A) ta' ea', refineEquiv {b | P ta b} ta' -> refineEquiv {b | P ea b} ea' -> refineEquiv {b | P (If cond Then ta Else ea) b} (If cond Then ta' Else ea').
proof: Proof. intros; setoid_rewrite refineEquiv_if with (f := fun cond : bool => {b : B | P (If cond Then ta Else ea) b}); eauto. reflexivity. Qed.
imports: Coq.Strings.String Coq.Sets.Ensembles Coq.Bool.Bool Fiat.Common Fiat.Common.BoolFacts Fiat.Common.LogicFacts Fiat.Computation.Core Fiat.Computation.Monad Fiat.Computation.SetoidMorphisms Fiat.Computation.Refinements.Tactics