proposition: Lemma refineEquiv_under_compose E B (monoid : Monoid B) (format1 format2 format2' : E -> Comp (B * E)) : (forall ctx', refineEquiv (format2 ctx') (format2' ctx')) -> forall ctx, refineEquiv (compose _ format1 format2 ctx) (compose _ format1 format2' ctx).
proof: Proof. unfold compose; intros. eapply refineEquiv_bind; [ reflexivity | ]. intro ab; destruct ab; simpl. eapply refineEquiv_bind; [ apply H | reflexivity ]. Qed.
imports: Fiat.Computation Fiat.Common.DecideableEnsembles Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.Notations