proposition: Lemma wlt_trans x : forall y z, wlt x y = true -> wlt y z = true -> wlt x z = true.
proof: Proof. intros. rewrite wlt_true_iff in *. unfold Word.wlt in *. eapply BinNat.N.lt_trans; eauto. Qed.
imports: Fiat.FiniteSetADTs.WordInterface Bedrock.Memory Bedrock.IL