proposition: Theorem empty_inv a s : empty (a :: s) -> ~ In a ref_list /\ empty s.
proof: Proof. intros H; split. - generalize (H (Pos 0 0)); unfold get; simpl; auto. - intro p; rewrite <- get_next with (a := a); auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia