proposition: Lemma wlt_irrefl x : wlt x x = false.
proof: Proof. unfold wlt, wltb. destruct (Word.wlt_dec x x). pose proof (Word.lt_le w); congruence. reflexivity. Qed.
imports: Fiat.FiniteSetADTs.WordInterface Bedrock.Memory Bedrock.IL