Goal:
  
  ============================
   (forall z : t,
    Eq = Lt ->
    match z with
    | ""%bs => Eq
    | String _ _ => Lt
    end = Lt -> match z with
                | ""%bs => Eq
                | String _ _ => Lt
                end = Lt)


DEBUG:Going to execute:
congruence