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