proposition: Lemma bv_ult_not_eqP : forall x y, bv_ultP x y -> x <> y.
proof: Proof. intros x y. unfold bv_ultP. case_eq (size x =? size y)%N; intros. - now apply ult_list_not_eqP in H0. - now contradict H0. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance