proposition: Lemma refineEquiv_compose_compose E B (monoid : Monoid B) (format1 format2 format3 : E -> Comp (B * E)) : forall ctx, refineEquiv (compose _ (compose _ format1 format2) format3 ctx) (compose _ format1 (compose _ format2 format3) ctx).
proof: Proof. unfold compose; intros. rewrite refineEquiv_bind2_bind. eapply refineEquiv_bind; [ reflexivity | ]. intro; rewrite refineEquiv_bind2_bind. symmetry; rewrite refineEquiv_bind2_bind. eapply refineEquiv_bind; [ reflexivity | ]. intro; rewrite refineEquiv_bind2_bind. rewrite refineEquiv_bind2_unit. eapply refineEquiv_bind; [ reflexivity | ]. intro; rewrite refineEquiv_bind2_unit; simpl. rewrite mappend_assoc; reflexivity. Qed.
imports: Fiat.Computation Fiat.Common.DecideableEnsembles Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.Notations