proposition: Theorem gen_cell_ordered: forall p, ordered_clause (gen_cell p).
proof: Proof. unfold gen_cell; elim ref_list; simpl. intros; red; apply olist_nil. intros a l Rec p; apply lit_insert_ordered; auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia