            P (==> T :type)]
     (have a (<=> (P x) (P y)) :by (Heq P))
     (have b (<=> (P y) (P x)) :by ((p/iff-sym (P x) (P y)) a))
-    (have c _ :discharge [P b])
-    (qed c)))
+    (qed b)))
 
 (defthm eq-trans
   "The transitivity property of equality."

           Q (==> U :type)]
    (assume [H2 (Q (f x))]
      (have a1 _ :by (eq-subst T (lambda [z T] (Q (f z))) x y))
      (have a2 (Q (f y)) :by (a1 H1 H2))
      (have a (==> (Q (f x)) (Q (f y))) :discharge [H2 a2]))
    (have b (equal T y x) :by ((eq-sym T x y) H1))
    (assume [H3 (Q (f y))]
      (have c1 _ :by (eq-subst T (lambda [z T] (Q (f z))) y x))
      (have c2 (Q (f x)) :by (c1 b H3))
      (have c (==> (Q (f y)) (Q (f x))) :discharge [H3 c2]))
    (have d (<=> (Q (f x)) (Q (f y))) :by ((p/iff-intro (Q (f x)) (Q (f y))) a c))
    (have e (equal U (f x) (f y)) :discharge [Q d])
    (qed e)))

    (have b (<=> (P y) (P z)) :by (H2 P))
    (have c (<=> (P x) (P z))
          :by ((p/iff-trans (P x) (P y) (P z)) a b))
    (qed c)))

(defthm eq-subst
  "Substitutivity property of equality."
