proposition: Theorem clause_insert_sat: forall v l s, sat (clause_insert v l) s <-> clause_sat v s /\ sat l s.
proof: Proof. intros v0 l s; split. intros H1; split. apply (H1 (length v0) v0). case (clause_insert_in (length v0, v0) v0 l); auto. intros n1 v1 H2. apply (H1 n1 v1). case (clause_insert_in (n1, v1) v0 l); auto. intros (H1, H2) n1 v1 H3. case (clause_insert_in (n1, v1) v0 l); auto. intros H4 _; case H4; clear H4; try intros H4; auto. injection H4; intros; subst; auto. apply (H2 n1 v1); auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia