Goal:
  
  ============================
   (forall x y : string, CompareSpec (x = y) (lt x y) (lt y x) (compare x y))


DEBUG:Going to execute:
induction x

Goals:
  
  ============================
   (forall y : string,
    CompareSpec (""%bs = y) (lt "" y) (lt y "") (compare "" y))

  
  b : Byte.byte
  x : string
  IHx : forall y : string,
        CompareSpec (x = y) (lt x y) (lt y x) (compare x y)
  ============================
   (forall y : string,
    CompareSpec (String b x = y) (lt (String b x) y) 
      (lt y (String b x)) (compare (String b x) y))


DEBUG:Going to execute:
destruct y

Goals:
  
  ============================
   (CompareSpec (""%bs = ""%bs) (lt "" "") (lt "" "") (compare "" ""))

    b : Byte.byte  y : string
  ============================
   (CompareSpec (""%bs = String b y) (lt "" (String b y))
      (lt (String b y) "") (compare "" (String b y)))

  
  b : Byte.byte
  x : string
  IHx : forall y : string,
        CompareSpec (x = y) (lt x y) (lt y x) (compare x y)
  ============================
   (CompareSpec (String b x = ""%bs) (lt (String b x) "")
      (lt "" (String b x)) (compare (String b x) ""))

  
  b : Byte.byte
  x : string
  IHx : forall y : string,
        CompareSpec (x = y) (lt x y) (lt y x) (compare x y)
  b0 : Byte.byte
  y : string
  ============================
   (CompareSpec (String b x = String b0 y) (lt (String b x) (String b0 y))
      (lt (String b0 y) (String b x)) (compare (String b x) (String b0 y)))


DEBUG:Going to execute:
simpl