proposition: Theorem fold_clause_insert1: forall (A: Set) (f: A -> clause) l1 l2 a, In a (fold_right (fun p l => clause_insert (f p) l) l2 l1) -> (exists b, exists n, In b l1 /\ a = (n, f b)) \/ In a l2.
proof: Proof. intros A f l1 l2 (n, l); generalize l2; elim l1; simpl; auto; clear l1 l2. intros a l1 Rec l2 H1. match goal with H: In ?p (clause_insert ?c ?cs) |- _ => case (clause_insert_in p c cs); intros tmp _; case (tmp H); clear tmp H end. intros tmp; left; exists a; exists n; injection tmp; intros; subst; auto. intros tmp; case (Rec l2); auto; clear tmp Rec. intros (b, (n1, (H1, H2))). left; exists b; exists n1; auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia