proposition: Lemma Refine_CorrectAlignedDecoderFormat {S} : forall (Invariant : S -> Prop) (FormatSpec FormatSpec' : FormatM S ByteString), EquivFormat FormatSpec FormatSpec' -> CorrectAlignedDecoderFor Invariant FormatSpec -> CorrectAlignedDecoderFor Invariant FormatSpec'.
proof: Proof. unfold EquivFormat; intros. exists (projT1 X), (projT1 (projT2 X)). pose proof (projT2 (projT2 X)). abstract (split_and; destruct_ex; intuition eauto; eexists; split; eauto; intros; eapply Specs.format_decode_correct_alt; try first [unfold flip, impl, pointwise_relation; reflexivity | unfold flip, impl, pointwise_relation; solve [eauto] | eapply EquivFormat_sym; eassumption]; eauto). Defined.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.NArith.NArith Coq.Arith.Arith Coq.Numbers.Natural.Peano.NPeano Coq.Logic.Eqdep_dec Fiat.Narcissus.Common.Specs Fiat.Narcissus.BinLib.Core Fiat.Narcissus.BinLib.AlignedByteString