proposition: Lemma INV_eq x1 x2 l1 l2 acc : INV (x1 :: l1) (x2 :: l2) acc -> X.eq x1 x2 -> INV l1 l2 (x1 :: acc).
proof: Proof. intros (U,V,W,X,Y) EQ. simpl in *. destruct (sorted_app_inv _ _ U) as (U1 & U2 & U3); auto. destruct (sorted_app_inv _ _ V) as (V1 & V2 & V3); auto. split; auto. - constructor; auto. apply InA_InfA with X.eq; auto_tc. - intros x y; inA; intros Hx [Hy|Hy]. + apply U3; inA. + apply X; inA. - intros x y; inA; intros Hx [Hy|Hy]. + rewrite Hy, EQ; apply V3; inA. + apply Y; inA. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat