proposition: Lemma BitString_into_ByteString_inj : forall l l', BitString_into_ByteString l = BitString_into_ByteString l' -> l = l'.
proof: Proof. induction l; destruct l'; simpl; intros; eauto. - apply (f_equal length_ByteString) in H; rewrite length_ByteString_push in H; compute in H; discriminate. - apply (f_equal length_ByteString) in H; rewrite length_ByteString_push in H; compute in H; discriminate. - apply (f_equal ByteString_pop) in H; rewrite !ByteString_mappend_push_pop_opt in H. injections; f_equal; eauto. 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