proposition: Theorem lit_is_in_correct: forall l c, ordered_clause c -> if (lit_is_in l c) then In l c else ~ In l c.
proof: Proof. intros l c H; unfold lit_is_in; apply is_in_correct; auto. exact lit_test_trans. intros; apply lit_test_anti_sym. exact lit_test_exact. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia