proposition: Lemma inter_list_spec x l1 l2 acc : sort X.lt (rev l1) -> sort X.lt (rev l2) -> (InA X.eq x (inter_list l1 l2 acc) <-> (InA X.eq x l1 /\ InA X.eq x l2) \/ InA X.eq x acc).
proof: Proof. revert l2 acc. induction l1 as [|x1 l1 IH1]. - intros l2 acc; simpl. inA. tauto. - induction l2 as [|x2 l2 IH2]; intros acc. * simpl. inA. tauto. * simpl. intros U V. destruct (sorted_app_inv _ _ U) as (U1 & U2 & U3); auto. destruct (sorted_app_inv _ _ V) as (V1 & V2 & V3); auto. case X.compare_spec; intro C. + rewrite IH1, !InA_cons, C; tauto. + rewrite (IH2 acc); auto. inA. intuition; try order. assert (X.lt x x1) by (apply U3; inA). order. + rewrite IH1; auto. inA. intuition; try order. assert (X.lt x x2) by (apply V3; inA). order. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat