simp only [def_iff_]
case h1.h1.a.a
x y : VarName
⊢ IsDeduct ∅
    ((((eq_ y y).and_ (eq_ x y)).imp_ ((eq_ y x).iff_ (eq_ y y))).imp_ ((eq_ y y).imp_ ((eq_ x y).imp_ (eq_ y x))))
case h1.h1.a.a
x y : VarName
⊢ IsDeduct ∅
    ((((eq_ y y).and_ (eq_ x y)).imp_ (((eq_ y x).imp_ (eq_ y y)).and_ ((eq_ y y).imp_ (eq_ y x)))).imp_
      ((eq_ y y).imp_ ((eq_ x y).imp_ (eq_ y x))))