proposition: Lemma INV_drop x1 l1 l2 acc : INV (x1 :: l1) l2 acc -> INV l1 l2 acc.
proof: Proof. intros (l1s,l2s,accs,l1a,l2a). simpl in *. destruct (sorted_app_inv _ _ l1s) as (U & V & W); auto. split; auto. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat