proposition: Theorem gen_rect_ordered: forall i z, ordered_clause (gen_rect i z).
proof: Proof. unfold gen_rect; intros i z; elim cross; simpl; auto. red; apply olist_nil. intros a s1 Rec. unfold ordered_clause, lit_insert; apply insert_olist; auto. exact lit_test_trans. intros; apply lit_test_anti_sym. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia