proposition: Lemma EquivFormat_Projection_Format (format : FormatM S' T) (f : S -> S') : EquivFormat (Projection_Format format f) (fun s => format (f s)).
proof: Proof. unfold EquivFormat, Projection_Format, Compose_Format; split; intros ? ?. apply unfold_computes. eexists; eauto. rewrite unfold_computes in H; destruct_ex; intuition; subst; eauto. Qed.
imports: Coq.ZArith.ZArith Coq.Strings.String Coq.Vectors.Vector Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.Narcissus.Common.Specs