proposition: Lemma combine_inj {sz sz'}: forall w00 w01 w10 w11, @combine sz w01 sz' w00 = combine w11 w10 -> w00 = w10 /\ w01 = w11.
proof: Proof. intros * Heq; split; [ apply (f_equal (@split2 sz sz')) in Heq | apply (f_equal (@split1 sz sz')) in Heq]; rewrite ?split1_combine, ?split2_combine in *; assumption. 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