simp only [def_and_]
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))))
case h1.h1.a.a
x y : VarName
⊢ IsDeduct ∅
    ((((eq_ y y).imp_ (eq_ x y).not_).not_.imp_
          (((eq_ y x).imp_ (eq_ y y)).imp_ ((eq_ y y).imp_ (eq_ y x)).not_).not_).imp_
      ((eq_ y y).imp_ ((eq_ x y).imp_ (eq_ y x))))