proposition: Lemma zext_inj {sz} {sz'} : forall (w w' : word sz), (zext w sz') = (zext w' sz') -> w = w'.
proof: Proof. unfold zext; intros * H. apply (f_equal (@Word.split1 _ _)) in H. rewrite !split1_combine in H. assumption. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat CertifiedExtraction.Extraction.BinEncoders.Basics Coq.Lists.List Bedrock.Word Program Nomega