proposition: Theorem fold_clause_insert_ordered: forall (A: Set) (f: A -> clause) l1 l2, (forall l, ordered_clause (f l)) -> ordered l1 -> ordered (fold_right (fun p l => clause_insert (f p) l) l1 l2).
proof: Proof. intros A f l1 l2 H; generalize l1; elim l2; simpl; auto; clear l1 l2. intros a l2 Rec l1 H1. apply clause_insert_ordered; auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia