printtree-fix

(in-package "STR")

(include-book "printtree")

(defthm printable->str-of-printable-fix
  (equal (printable->str (printable-fix x))
    (printable->str x))
  :hints (("Goal" :in-theory (enable printable->str printable-fix))))

(defthm printtree->str-of-printtree-fix
  (equal (printtree->str (printtree-fix x))
    (printtree->str x))
  :hints (("Goal" :in-theory (enable printtree->str printtree-fix))))