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