proposition: Theorem length_clauses_update: forall l c cs, length (clauses_update l c cs) <= length cs.
proof: Proof. intros l c cs; elim cs; simpl; auto. intros (n1, c1) cs1 Rec; case (lit_is_in l c1); auto with arith. apply Nat.le_trans with (2 := (le_n_S _ _ Rec)). rewrite length_clause_insert; auto with arith. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia