proposition: Theorem clauses_merge_sat: forall cs1 cs2 s, sat (clauses_merge cs1 cs2) s <-> sat cs1 s /\ sat cs2 s.
proof: Proof. intros cs1 cs2 s; split; [intros H; split | intros (H, H1)]. intros n c H1; apply (H n c). case (clauses_merge_in (n, c) cs1 cs2); auto. intros n c H1; apply (H n c). case (clauses_merge_in (n, c) cs1 cs2); auto. intros n c H2. case (clauses_merge_in (n, c) cs1 cs2); auto. intros tmp _; case tmp; auto; clear tmp; intros H3. apply (H n c); auto. apply (H1 n c); auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia