proposition: Lemma refineEquiv_if A : forall (f : bool -> Comp A) (b : bool) ta ea, refineEquiv (f true) ta -> refineEquiv (f false) ea -> refineEquiv (f b) (If b Then ta Else ea).
proof: Proof. destruct b; simpl; auto. 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