proposition: Lemma encoder_empty_cache_OK {S1 S2} (format_A : FormatM S1 ByteString) (format_B : FormatM S2 ByteString) (encode_B : forall sz, AlignedEncodeM sz) (encoder_B_OK : CorrectAlignedEncoder format_B encode_B) : forall (s1 : S1) (s2 : S2) (env : CacheFormat) (tenv' tenv'' : ByteString * CacheFormat), format_B s2 env ∋ tenv' -> format_A s1 (snd tenv') ∋ tenv'' -> exists tenv3 tenv4 : _ * CacheFormat, projT1 encoder_B_OK s2 env = Some tenv3 /\ format_A s1 (snd tenv3) ∋ tenv4.
proof: Proof. intros. destruct tenv'; destruct tenv''; simpl in *. match goal with |- exists _ _, ?b = _ /\ _ => destruct b as [ [? ?] | ] eqn: ? end. - eexists _, _; simpl in *; split; intros; eauto. simpl in *. destruct c; destruct c1; eauto. - eapply (proj1 (projT2 encoder_B_OK)) in Heqo. eapply Heqo in H; intuition. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Narcissus.BinLib Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Common.ComposeCheckSum Fiat.Narcissus.Common.ComposeIf Fiat.Narcissus.Formats Fiat.Narcissus.BaseFormats Fiat.Narcissus.Automation.Solver Fiat.Narcissus.Automation.NormalizeFormats Bedrock.Word