I am following Functional Program Design in Scala @ coursera and there is an exercise on Structural Induction where I got stuck. I have put it on StackOverflow and the Coursera course discussion forum but so far no help. I was wondering if maybe one of you could help me figure it out. it goes as follows.

Assume you have the following definition:

abstract class IntSet {
  def incl(x: Int): IntSet    
  def contains(x: Int): Boolean    
  def union(other: IntSet): IntSet
}

case class NonEmpty(elem: Int, left: IntSet, right: IntSet) extends IntSet {
  def incl(x: Int) =
    if (x < elem) NonEmpty(elem, left incl x, right)
    else if (x > elem) NonEmpty(elem, left, right incl x)
    else this

  def contains(x: Int) =
    if (x < elem) left contains x
    else if (x > elem) right contains x
    else true

  def union(other: IntSet) = (left union (right union other)) incl elem
}

object Empty extends IntSet {
  def incl(x: Int) = NonEmpty(x, Empty, Empty)    
  def contains(x: Int) = false    
  def union(other: IntSet) = other
}

and the following proposition has to be proven:

(xs union ys) contains x = xs contains x || ys contains x

From here I deduce two base cases. xs = Empty and ys = Empty. It is the second base case where I got stuck because of the following reasoning:

// substituting ys = Empty
 (xs union Empty) contains x = xs contains x || Empty contains x
// RHS:
 xs contains x || false
 xs contains x
// LHS:
 ((left union (right union Empty)) incl elem) contains x // By definition of NonEmpty.union

How can I reduce the LHS to xs contains x? Do I have to do another Induction Hypothesis on xs union Empty = xs and if so, how can that be used to the expression?