proposition: Lemma BtoW_inj : forall (v v' : B), BtoW v = BtoW v' -> v = v'.
proof: Proof. intros; eapply zext_inj; apply H. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat CertifiedExtraction.Extraction.BinEncoders.Basics Coq.Lists.List Bedrock.Word Program Nomega