proposition: Theorem out_not_in_refl: ~ In out ref_list.
proof: Proof. unfold ref_list; intros H. case (in_progression size 1 out). intros tmp _; case (tmp H); auto; clear tmp. intros H1; contradict H1; auto with arith. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia