proposition: Theorem clause_merge_valid: forall c1 c2 s, valid_clause c1 s -> valid_clause c2 s -> valid_clause (clause_merge c1 c2) s.
proof: Proof. intros c1 c2 s H H1 l Hl. case (clause_merge_in l c1 c2); auto. intros tmp _; case tmp; auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia