attempt binary proof. last statement seems true but how do I deal with S constructor? also have never inducted on type with > 2 constructors