proposition: Lemma BitString_into_ByteString_eq : forall l, l = ByteString_into_BitString (BitString_into_ByteString l).
proof: Proof. induction l; simpl; try reflexivity. rewrite IHl, <- ByteString_into_BitString_eq; clear IHl. destruct (BitString_into_ByteString l). unfold ByteString_push; simpl. destruct (eq_nat_dec padding0 7) eqn: ?. - unfold ByteString_into_BitString; simpl. f_equal; subst. shatter_word front0; reflexivity. - 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.Narcissus.Common.Specs