proposition: Lemma refine_Projection_Format {cache : Cache} {S S' T : Type} (f : S -> S') (format : FormatM S' T) : forall s env, refineEquiv (Projection_Format format f s env) (format (f s) env).
proof: Proof. unfold Projection_Format, Compose_Format; intros; split. - intros v Comp_v. apply unfold_computes; eexists; intuition eauto. - intros v Comp_v. rewrite unfold_computes in Comp_v; destruct_ex; intuition eauto. subst; eauto. Qed.
imports: Coq.ZArith.ZArith Coq.Strings.String Coq.Vectors.Vector Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.Narcissus.Common.Specs