proposition: Lemma sequence_Encoding_padding_0 {cache : Cache} {S : Type} enc1 enc2 (enc1_aligned : forall s ce t ce', enc1 s ce = Some (t, ce') -> padding t = 0) (enc2_aligned : forall s ce t ce', enc2 s ce = Some (t, ce') -> padding t = 0) : forall s ce b ce', @sequence_Encode ByteString cache _ S enc1 enc2 s ce = Some (b, ce') -> padding b = 0.
proof: Proof. unfold sequence_Encode. intros. destruct enc1 eqn:?; destruct_conjs; [| discriminate]; simpl in *. destruct enc2 eqn:?; destruct_conjs; [| discriminate]; simpl in *. injections. apply enc1_aligned in Heqo. apply enc2_aligned in Heqo0. rewrite ByteString_enqueue_ByteString_padding_eq. rewrite Heqo. rewrite Heqo0. reflexivity. 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