proposition: Lemma refineEquiv_decides_eqb (b b1 b2 : bool) : decides b (b1 = b2) <-> b = If b2 Then b1 Else negb b1.
proof: Proof. destruct_head bool; simpl; intuition. 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