proposition: Lemma ByteString_mappend_pop_opt_inj : forall (t : bool) (m b b' : ByteString), ByteString_pop b = Some (t, m) -> ByteString_pop b' = Some (t, m) -> b = b'.
proof: Proof. destruct b; destruct b'. unfold ByteString_pop; simpl padding; simpl paddingOK; simpl front; simpl byteString. destruct padding0; destruct padding1. - destruct byteString0; intros; try discriminate. destruct byteString1; try discriminate. injection H; injection H0; intros. subst. injection H3; intros. apply inj_pair2_eq_dec in H2; eauto. f_equal. rewrite (shatter_word_0 front0); rewrite (shatter_word_0 front1); reflexivity. apply le_uniqueness_proof. rewrite (shatter_word c) in *; rewrite (shatter_word c0) in *. injection H3; intros. rewrite H1; f_equal. f_equal. simpl in H4; rewrite H4; reflexivity. apply inj_pair2_eq_dec in H6; eauto. apply eq_nat_dec. apply eq_nat_dec. - destruct byteString0; intros; try discriminate. injection H; injection H0; intros. rewrite <- H1 in H3; injection H3; intros. exfalso. generalize H7 paddingOK1; clear; intro; rewrite H7. intros; omega. - destruct byteString1; intros; try discriminate. injection H; injection H0; intros. rewrite <- H1 in H3; injection H3; intros. exfalso. generalize H7 paddingOK0; clear; intro; rewrite H7. intros; omega. - intros; injection H; injection H0; intros. rewrite <- H1 in H3; injection H3; intros; subst. repeat f_equal. rewrite (shatter_word front0); rewrite (shatter_word front1); f_equal; eauto. apply inj_pair2_eq_dec in H6; eauto. apply eq_nat_dec. 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