proposition: Lemma ult_list_trans : forall x y z, ult_list x y = true -> ult_list y z = true -> ult_list x z = true.
proof: Proof. unfold ult_list. intros x y z. apply ult_list_big_endian_trans. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance