proposition: Theorem lit_insert_valid: forall l c s, valid_lit l s -> valid_clause c s -> valid_clause (lit_insert l c) s.
proof: Proof. intros l; case l; simpl. intros p z c s (H1, (H2, H3)) H4 l1; case l1; simpl. intros p1 z1 H5. unfold lit_insert in H5; case insert_inv with (1 := H5); auto. intros tmp; injection tmp; intros; subst; clear tmp; auto. intros H6; apply (H4 (L p1 z1) H6). Qed.
imports: List UList Permutation Div OrderedList ListOp Lia