proposition: Lemma ByteString_mappend_push_pop_opt : forall (t : bool) (m : ByteString), ByteString_pop (ByteString_push t m) = Some (t, m).
proof: Proof. destruct m; simpl. unfold ByteString_push; unfold ByteString_pop. simpl. simpl padding. destruct (eq_nat_dec padding0 7); simpl padding; simpl paddingOK; simpl front; simpl byteString. - subst; simpl; repeat f_equal. apply le_uniqueness_proof. - simpl; repeat f_equal. apply le_uniqueness_proof. 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