proposition: Theorem length_clauses_merge: forall cs1 cs2, length (clauses_merge cs1 cs2) = length cs1 + length cs2.
proof: Proof. intros cs1 cs2; unfold clauses_merge; apply add_length. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia