proposition: Lemma refineEquiv_If_Then_Else_ThenC : forall (E B : Type) (monoid : Monoid B) (format1 format2 format3 : E -> Comp (B * E)) (ctx : E) b, refineEquiv (((If b Then format1 Else format2) ThenC format3) ctx) (If b Then ((format1 ThenC format3) ctx) Else ((format2 ThenC format3) ctx)).
proof: Proof. intros; destruct b; reflexivity. Qed.
imports: Fiat.Computation Fiat.Common.DecideableEnsembles Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.Notations