proposition: Theorem fold_clause_insert3: forall (A: Set) (f: A -> clause) l1 l2 a, In a l1 -> In (length (f a), (f a)) (fold_right (fun p l => clause_insert (f p) l) l2 l1).
proof: Proof. intros A f l1 a l2; generalize l2; elim l1; simpl; auto; clear l1 l2. intros l2 H; case H. intros b l1 Rec l2 [H | H]; subst; match goal with |- In ?p (clause_insert ?c ?cs) => case (clause_insert_in p c cs); intros _ tmp; apply tmp; clear tmp; auto end. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia