proposition: Theorem fold_insert1: forall (A: Set) (f: A -> lit) a l, In a l -> In (f a) (fold_right (fun p l => lit_insert (f p) l) nil l).
proof: Proof. intros A f a l; elim l; simpl; auto with arith; clear l. intros b l1 Rec [H | H]; subst; match goal with |- In ?X (lit_insert ?Y ?Z) => case (lit_insert_in X Y Z); intros _ tmp; apply tmp; clear tmp; auto end. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia