proposition: Theorem clauses_update_ordered: forall l c cs, ordered_clause c -> ordered cs -> ordered (clauses_update l c cs).
proof: Proof. Proof with auto with datatypes. intros l c cs; elim cs; simpl... intros (n1, c1) cs1 Rec H H1; case (lit_is_in l c1). apply Rec... intros n2 c2 H2; apply (H1 n2 c2)... apply clause_insert_ordered... apply lit_rm_ordered... apply (H1 n1 c1)... apply Rec... intros n2 c2 H2; apply (H1 n2 c2)... Qed.
imports: List UList Permutation Div OrderedList ListOp Lia