proposition: Lemma wlt_true_iff : forall x y, wlt x y = true <-> Word.wlt x y.
proof: Proof. intros. unfold wlt, IL.wltb. destruct (Word.wlt_dec x y); intuition. Qed.
imports: Fiat.FiniteSetADTs.WordInterface Bedrock.Memory Bedrock.IL