proposition: Theorem clauses_merge_valid: forall cs1 cs2 s, valid cs1 s -> valid cs2 s -> valid (clauses_merge cs1 cs2) s.
proof: Proof. intros cs1 cs2 s H H1 n1 c1 Hc1. case (clauses_merge_in (n1, c1) cs1 cs2); auto. intros tmp _; case tmp; clear tmp; auto; intros H2. apply (H n1 c1); auto. apply (H1 n1 c1); auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia