proposition: Lemma AlignedEncoder_some_inv' {S} {cache : Cache} (enc' : EncodeM S ByteString) (enc : forall sz, AlignedEncodeM sz) (enc_OK : EncodeMEquivAlignedEncodeM enc' enc) : forall sz (t : Vector.t Core.char sz) n1 (s : S) v ni ce ce', enc _ t n1 s ce = Some (v, ni, ce') -> exists b ce', enc' s ce = Some (b, ce').
proof: Proof. intros. destruct (enc' s ce) eqn:?; destruct_conjs; eauto. eapply enc_OK in Heqo. rewrite Heqo in H. discriminate. Qed.
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.Common.BoundedLookup Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Common.ComposeIf Fiat.Narcissus.BaseFormats Fiat.Narcissus.BinLib.Core Fiat.Narcissus.BinLib.AlignedByteString