proposition: Theorem clause_merge_ordered: forall c1 c2, ordered_clause c1 -> ordered_clause c2 -> ordered_clause (clause_merge c1 c2).
proof: Proof. intros c1 c2 H1 H2; unfold ordered_clause, clause_merge; apply merge_olist; auto. exact lit_test_trans. intros; apply lit_test_anti_sym. exact lit_test_exact. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia