proposition: Lemma CorrectEncoder_Fix (encode_body : EncodeM S T -> EncodeM S T) (format_body : FormatM S T -> FormatM S T) (format_body_OK : Frame.monotonic_function (format_body : funType [S; CacheFormat] (T * CacheFormat) -> funType [S; CacheFormat] (T * CacheFormat))) (measure : S -> nat) (encode_body_correct : forall n encode, (CorrectEncoder (Restrict_Format (fun s => measure s < n) (Fix_Format format_body)) encode) -> CorrectEncoder (Restrict_Format (fun s => measure s < Datatypes.S n) (format_body (Fix_Format format_body))) (encode_body encode)) : CorrectEncoder (Fix_Format format_body) (Fix_Encode measure encode_body).
proof: Proof. split; intros. - destruct (CorrectEncoder_Fix' encode_body format_body format_body_OK measure encode_body_correct (Datatypes.S (measure a))) as [? _]; eauto. eapply H0 in H; try solve [unfold Compose_Target; apply unfold_computes; split; eauto]. unfold Restrict_Format, Compose_Format in H. rewrite @unfold_computes in H. destruct_ex; split_and; subst; eauto. - destruct (CorrectEncoder_Fix' encode_body format_body format_body_OK measure encode_body_correct (Datatypes.S (measure a))) as [_ ?]; eauto. eapply H0 in H; try solve [simpl; unfold Fix_Encode in H0; eauto]. intro; eapply H. unfold Restrict_Format, Compose_Format; apply unfold_computes. eexists; split_and; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Strings.String Coq.Vectors.Vector Fiat.Computation Fiat.Narcissus.Common.Specs Fiat.Narcissus.Formats.Base.FMapFormat Fiat.Computation.FixComp