proposition: Lemma wlt_trans x : forall y z, wlt x y = true -> wlt y z = true -> wlt x z = true.
proof: Proof. induction x; intros [|?] [|?]; simpl; intros; try congruence. eapply IHx; eassumption. Qed.
imports: Fiat.FiniteSetADTs.WordInterface