proposition: Theorem gen_cell_correct: forall l x y, (In l (gen_cell (Pos x y)) <-> exists z, l = L (Pos x y) z /\ (In z ref_list)).
proof: Proof. intros l x y; unfold gen_cell; split. intros H2. case (fold_insert2 _ (fun p => (L (Pos x y) p)) _ _ H2); clear H2; intros b (Hb, Hb1); exists b; auto. intros (b, (Hb1, Hb2)); rewrite Hb1; clear Hb1. apply fold_insert1 with (f := (fun p => L (Pos x y) p)); auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia