proposition: Theorem valid_update: forall p z c s, valid_clause c s -> valid_pos p -> (forall z, In z ref_list -> ~ In (L p z) c) -> valid_clause c (update p z s).
proof: Proof. intros p z c s H H1 H2 l Hl. generalize (H l Hl) Hl; clear H Hl. case l; simpl. intros p1 z1 (H3, (H4, H5)) H6; split; auto. rewrite update_diff_get; auto. intro tmp; subst; case (H2 z1); auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia