proposition: Lemma ByteString_mappend_push_step_opt : forall (t : bool) (m n : ByteString), mappend (ByteString_push t m) n = ByteString_push t (mappend m n).
proof: Proof. intros t m n; destruct (ByteString_mappend_push_eq t m). simpl mappend. rewrite H, <- ByteString_mappend_assoc. destruct (ByteString_mappend_push_eq t (mappend m n)). simpl mappend in *; rewrite H0. 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