proposition: Lemma union_list_spec x l1 l2 acc : InA X.eq x (union_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. rewrite rev_append_rev. inA. tauto. - induction l2 as [|x2 l2 IH2]; intros acc; simpl. * rewrite rev_append_rev. inA. tauto. * case X.compare_spec; intro C. + rewrite IH1, !InA_cons, C; tauto. + rewrite (IH2 (x2::acc)), !InA_cons. tauto. + rewrite IH1, !InA_cons; tauto. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat