proposition: Lemma proper_consumer_t_None' {C} (t' : forall {numBytes}, AlignedDecodeM C numBytes) (t'_OK : forall (numBytes_hd n0 : nat) (v0 : Vector.t char (S numBytes_hd)) (cd0 : CacheDecode), @t' (S numBytes_hd) v0 (S n0) cd0 = (Ifopt @t' numBytes_hd (Vector.tl v0) n0 cd0 as a0 Then Some (fst (fst a0), S (snd (fst a0)), snd a0) Else None)) : forall {n m} (v : ByteBuffer.t (m + n)) (v1 : Vector.t char m) (v2 : Vector.t char n) cd, t' v m cd = None -> build_aligned_ByteString v = build_aligned_ByteString (Vector.append v1 v2) -> t' v2 0 cd = None.
proof: Proof. intros. apply build_aligned_ByteString_inj in H0; subst. revert n v2 cd H; induction v1. - simpl; intros; eauto. - simpl; intros. rewrite t'_OK in H. eapply IHv1. simpl in *; destruct (t' (n + n0) (Vector.append v1 v2) n cd) as [ [ [? ?] ?] | ]; simpl in *; eauto; 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.Narcissus.Common.Specs Fiat.Narcissus.BinLib.Core Fiat.Narcissus.BinLib.AlignedByteString