proposition: Theorem clauses_update_sat_rev: forall l c cs s, ordered_clause c -> lit_sat l s -> ordered cs -> (forall l, In l c -> ~ lit_sat l s) -> sat cs s -> sat (clauses_update l c cs) s.
proof: Proof. intros l c cs s H1 H2 H3 H4; generalize H3; elim cs; simpl; auto; clear H3. intros (n1, c1) cs1 Rec H3 H5. assert (F1: ordered_clause c1). apply (H3 n1); auto with datatypes. generalize (lit_is_in_correct l c1 F1). case (lit_is_in l c1); auto; intros H6; auto. apply Rec; auto. intros n3 c3 Hn3; apply (H3 n3); auto with datatypes. intros n2 c2 Hn2; apply (H5 n2); auto with datatypes. match goal with |- context[sat (clause_insert ?X ?Y) ?Z] => case (clause_insert_sat X Y Z); intros _ U2; apply U2; clear U2 end. split. case (lit_rm_sat c c1 s); auto. intros H7 _; apply H7; clear H7. apply (H5 n1 c1); auto with datatypes. apply Rec. intros n3 c3 Hn3; apply (H3 n3); auto with datatypes. intros n2 c2 Hn2; apply (H5 n2 c2); auto with datatypes. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia