Goal:
  
  ============================
   (forall x : t, parse (print x) = x)


DEBUG:Going to execute:
induction x

Goals:
  
  ============================
   (parse (print EmptyString) = EmptyString)

    b : Byte.byte  x : t  IHx : parse (print x) = x
  ============================
   (parse (print (String b x)) = String b x)


DEBUG:Going to execute:
simpl

Goals:
  
  ============================
   (EmptyString = EmptyString)

    b : Byte.byte  x : t  IHx : parse (print x) = x
  ============================
   (String b (parse (print x)) = String b x)


DEBUG:Going to execute:
intros

Goals:
  
  ============================
   (EmptyString = EmptyString)

    b : Byte.byte  x : t  IHx : parse (print x) = x
  ============================
   (String b (parse (print x)) = String b x)


DEBUG:Going to execute:
auto

Goals:
  
  ============================
   (EmptyString = EmptyString)

    b : Byte.byte  x : t  IHx : parse (print x) = x
  ============================
   (String b (parse (print x)) = String b x)


DEBUG:Going to execute:
<coq-core.plugins.ltac::auto@0> $1 $2 $3