proposition: Lemma refineEquiv_compose_Done E B (monoid : Monoid B) (format2 : E -> Comp (B * E)) : forall ctx, refineEquiv (compose _ (fun ctx => ret (mempty, ctx)) format2 ctx) (format2 ctx).
proof: Proof. unfold compose; simpl; intros. rewrite refineEquiv_bind2_unit; simpl. split; unfold Bind2; intros v Comp_v. - computes_to_econstructor; eauto; destruct v; simpl; rewrite mempty_left; eauto. - computes_to_inv; subst; destruct v0; rewrite mempty_left; eauto. Qed.
imports: Fiat.Computation Fiat.Common.DecideableEnsembles Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.Notations