proposition: Lemma inter_list_ok l1 l2 acc : INV l1 l2 acc -> sort X.lt (inter_list l1 l2 acc).
proof: Proof. revert l2 acc. induction l1 as [|x1 l1 IH1]; [|induction l2 as [|x2 l2 IH2]]; simpl. - eauto. - eauto. - intros acc inv. case X.compare_spec; intro C. * apply IH1. eapply INV_eq; eauto. * apply (IH2 acc). eapply INV_sym, INV_drop, INV_sym; eauto. * apply IH1. eapply INV_drop; eauto. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat