proposition: Corollary CorrectEncoder_Projection_Format (format : FormatM S' T) (encode : EncodeM S' T) (g : S -> S') : CorrectEncoder format encode -> CorrectEncoder (Projection_Format format g) (compose encode g).
proof: Proof. intros; replace (compose encode g) with (Compose_Encode encode (fun s => Some (g s))). eapply CorrectEncoder_Compose; intros; try (destruct (DecideableEnsembles.dec s') eqn: ?; first [discriminate | injections]); intuition eauto. apply functional_extensionality; intros; reflexivity. Qed.
imports: Coq.ZArith.ZArith Coq.Strings.String Coq.Vectors.Vector Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.Narcissus.Common.Specs