proposition: Theorem lit_rm_valid: forall c1 c2 s, ordered_clause c1 -> ordered_clause c2 -> valid_clause c2 s -> valid_clause (lit_rm c1 c2) s.
proof: Proof. intros c1 c2 s H H1 H2 l H3. case (lit_rm_in l c1 c2); auto. intros tmp _; case tmp; auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia