proposition: Theorem empty_cons a s : ~ In a ref_list -> empty s -> empty (a :: s).
proof: Proof. intros Ha H p; case p; intros x y; case y; simpl. - case x; unfold get; simpl; auto. intros x1. rewrite Nat.add_0_r. generalize (H (Pos x1 (pred size))); unfold get; simpl; case size; simpl. + rewrite Nat.mul_0_r; simpl;auto. + intros n1; rewrite (Nat.add_comm n1); auto. - intros y1; generalize (H (Pos x y1)); unfold get; simpl. rewrite <- plus_n_Sm; auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia