proposition: Lemma WS_match_eq_refl {sz sz'} : forall b (w: word sz) (w': word sz') (eql: sz = sz') (eqlS: S sz = S sz'), w = match eql in _ = y return (word y -> word sz) with | eq_refl => fun x: word sz => x end w' -> WS b w = match eqlS in _ = y return (word y -> word (S sz)) with | eq_refl => fun x: word (S sz) => x end (WS b w').
proof: Proof. intros. destruct eql; subst. rewrite (UIP_nat _ _ eqlS eq_refl). reflexivity. 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