proposition: Theorem lit_rm_in: forall l c1 c2, ordered_clause c1 -> ordered_clause c2 -> (In l (lit_rm c1 c2) <-> ~In l c1 /\ In l c2).
proof: Proof. unfold ordered_clause, lit_rm; intros l c1 c2 H H1; split; intros H2. split. contradict H2; apply rm_not_in; auto. exact lit_test_trans. intros; apply lit_test_anti_sym; auto. exact lit_test_exact. apply (rm_incl _ lit_test c1 c2 l); auto. case H2; clear H2; intros H2 H3. apply rm_in; auto. exact lit_test_exact. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia