apply specId y
case h1.h1.h1.a.a.h1
x y z : VarName
⊢ IsDeduct ∅ (forall_ z (((eq_ x y).and_ (eq_ z z)).imp_ ((eq_ x z).iff_ (eq_ y z))))
case h1.h1.h1.a.a.h1.h1
x y z : VarName
⊢ IsDeduct ∅ (forall_ y (forall_ z (((eq_ x y).and_ (eq_ z z)).imp_ ((eq_ x z).iff_ (eq_ y z)))))