proposition: Lemma checksum'_somewhat_injective : forall x y0 y1 z, fst y0 <> wzero 8 \/ snd y0 <> wzero 8 -> fst y1 <> wzero 8 \/ snd y1 <> wzero 8 -> checksum' (x ++ y0 :: z) = checksum' (x ++ y1 :: z) -> y0 = y1.
proof: Proof. intros * ? ? H. rewrite !(checksum'_app _ (_ :: _)), <- !app_comm_cons in H. simpl in H; apply add_bytes_into_checksum_inj_l in H; try assumption. destruct y0, y1, H; simpl in *; congruence. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat List Bedrock.Word Coq.ZArith.ZArith Coq.micromega.Psatz NArith NArithRing ZArith ZArithRing Program Coq.micromega.Psatz AlignedByteString Permutation