proposition: Theorem lit_rm_sat: forall l1 l2 s, ordered_clause l1 -> ordered_clause l2 -> (forall ll, In ll l1 -> ~ lit_sat ll s) -> (clause_sat l2 s <-> clause_sat (lit_rm l1 l2) s).
proof: Proof. intros l1 l2 s O1 O2 H; split; intros (ll,(H2, H3)); exists ll; split; auto. case (lit_rm_in ll l1 l2); auto; intros _ H4; apply H4; auto. split; auto. intros H5; case (H ll); auto. case (lit_rm_in ll l1 l2); auto; intros H4 _; case H4; auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia